Diff 1.0.2 → 2.0.0
raw patch · 10 files changed
+1129/−193 lines, 10 filesdep −Diffdep −QuickCheckdep −array
Dependencies removed: Diff, QuickCheck, array, base, directory, pretty, process, test-framework, test-framework-quickcheck2
Files
- Diff-liquidhaskell/Diff-liquidhaskell.cabal +38/−0
- Diff.cabal +27/−12
- README.md +53/−0
- bench/bench.hs +33/−0
- src/Data/Algorithm/Diff.hs +592/−66
- src/Data/Algorithm/Diff/Refinement.hs +93/−0
- src/Data/Algorithm/Diff/Type.hs +33/−0
- src/Data/Algorithm/DiffContext.hs +135/−46
- src/Data/Algorithm/DiffOutput.hs +111/−31
- test/Test.hs +14/−38
+ Diff-liquidhaskell/Diff-liquidhaskell.cabal view
@@ -0,0 +1,38 @@+cabal-version: 2.4+name: Diff-liquidhaskell+version: 0.1.0.0+synopsis: LiquidHaskell static checks for the Diff package+description:+ Provides a test suite whose build executes Diff's LiquidHaskell refinement type+ annotation checks.+ Exists as a separate package to break the cyclic dependency:+ Diff -> liquidhaskell -> liquidhaskell-boot -> Diff.+build-type: Simple++tested-with: GHC == 9.14.1++library+ default-language: Haskell2010+ -- Re-use the main Diff source tree so LiquidHaskell checks the real code.+ hs-source-dirs: ../src+ -- No modules are exposed because this package is intended+ -- for checking the build only.+ other-modules:+ Data.Algorithm.Diff+ Data.Algorithm.Diff.Refinement+ Data.Algorithm.Diff.Type+ Data.Algorithm.DiffOutput+ Data.Algorithm.DiffContext+ build-depends:+ base >= 4.22.0.0 && < 5+ , array+ , pretty >= 1.1+ -- LH version scheme: 0.<GHC_VERSION>.<LH_REVISION>+ -- Update the corresponding versions in .github/workflows/liquidhaskell.yml+ -- after upgrading GHC and LH to keep CI in sync.+ , liquidhaskell ^>= 0.9.14.1.1+ -- Recompilation check is disabled to make sure changes to specification+ -- annotations are checked by the LH plugin (otherwise they are silently ignored+ -- if no source change is introduced).+ -- All warnings are disabled to focus on LH output.+ ghc-options: -fplugin=LiquidHaskell -O0 -fforce-recomp -w
Diff.cabal view
@@ -1,24 +1,28 @@-Cabal-Version: 1.18+Cabal-Version: 3.14 name: Diff-version: 1.0.2+version: 2.0.0 synopsis: Diff algorithm in pure Haskell description: Implementation of the standard diff algorithm in Haskell. . Time complexity is O(ND) (input length * number of differences). Space complexity is O(D^2). Includes utilities for pretty printing. category: Algorithms-homepage: https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.6927-license: BSD3+homepage: https://web.archive.org/web/20150326181224/http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.6927+license: BSD-3-Clause license-file: LICENSE author: Sterling Clover maintainer: David Fox <dsf@seereason.com>-Build-Type: Simple+build-Type: Simple+extra-doc-files: README.md, CHANGELOG.md+extra-files: ./Diff-liquidhaskell/Diff-liquidhaskell.cabal+bug-reports: https://github.com/seereason/Diff/issues tested-with:- GHC == 9.12.0- GHC == 9.10.1- GHC == 9.8.2- GHC == 9.6.6+ GHC == 9.14.1+ GHC == 9.12.2+ GHC == 9.10.3+ GHC == 9.8.4+ GHC == 9.6.7 GHC == 9.4.8 GHC == 9.2.8 GHC == 9.0.2@@ -27,8 +31,6 @@ GHC == 8.6.5 GHC == 8.4.4 -extra-doc-files: CHANGELOG.md- library default-language: Haskell2010 build-depends:@@ -37,9 +39,11 @@ , pretty >= 1.1 hs-source-dirs: src exposed-modules:- Data.Algorithm.Diff,+ Data.Algorithm.Diff Data.Algorithm.DiffOutput Data.Algorithm.DiffContext+ other-modules: Data.Algorithm.Diff.Refinement+ Data.Algorithm.Diff.Type ghc-options: -Wall -funbox-strict-fields source-repository head@@ -61,3 +65,14 @@ , QuickCheck , test-framework , test-framework-quickcheck2++benchmark simple+ default-language: Haskell2010+ type: exitcode-stdio-1.0+ main-is: bench/bench.hs+ build-depends:+ Diff+ , base >= 3 && <= 6+ , criterion+ , deepseq+ , random
+ README.md view
@@ -0,0 +1,53 @@+## Diff++This is an implementation of the standard diff algorithm in Haskell.++Time complexity is O(ND) (input length * number of differences). Space complexity is O(D^2). Includes utilities for pretty printing.++### Building & testing++Build with++```shell+cabal build+```++Test with++```shell+cabal test+```++Benchmark with++```shell+cabal bench+```++### Checking Diff with LiquidHaskell++The Diff source code can we checked with [LiquidHaskell](https://ucsd-progsys.github.io/liquidhaskell/).++LiquidHaskell requires `ghc` version 9.14.1, and an SMT solver. We have tested+the checks with the [Z3](https://github.com/Z3Prover/z3) SMT solver (versions 4.16,+and 4.15.1).++```+cd Diff-liquidhaskell && cabal build+```++The `Diff-liquidhaskell` package is a device to avoid the circular dependency between+`liquidhaskell` and the `Diff` package.++``` mermaid+flowchart LR+ Diff --> liquidhaskell --> liquidhaskell-boot --> Diff+```++Contributions that update the LiquidHaskell checks are appreciated but not required at this point.++### Acknowledgments++The LiquidHaskell static checks were designed and implemented with the support of+[Tweag](https://www.tweag.io/), a part of [Modus Create](https://www.moduscreate.com/).+Learn more in this [blog post](https://www.tweag.io/blog/2026-06-11-diff-package-static-checks/).
+ bench/bench.hs view
@@ -0,0 +1,33 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+-- {-# OPTIONS_GHC -Wno-orphans #-}++module Main where++import Criterion.Main+import Control.DeepSeq+import GHC.Generics+import System.Random++import Data.Algorithm.Diff++deriving instance Generic (Diff a)++instance NFData a => NFData (Diff a)++main :: IO ()+main = doBenchMarks 37++doBenchMarks :: Int -> IO ()+doBenchMarks seed =+ let rbools = randoms (mkStdGen seed) :: [Bool]+ (s1000_1, rbools1) = splitAt 1000 rbools+ (s1000_2, rbools2) = splitAt 1000 rbools1+ s500_2 = take 500 s1000_2+ in (s1000_1, s1000_2, s500_2) `deepseq` defaultMain+ [ bgroup "diff bool lists"+ [ bench "1000 bools" $ nf (getDiff s1000_1) s1000_2+ , bench "1000/500 bools" $ nf (getDiff s1000_1) s500_2+ ]+ ]
src/Data/Algorithm/Diff.hs view
@@ -1,3 +1,8 @@+{-@ LIQUID "--ple" @-}+-- Import of the 'Data.Algorithm.Diff.Refinement' module is required for LiquidHaskell+-- specifications in this module, but is unused in the actual code.+-- The following GHC option suppresses the unused import warning.+{-# OPTIONS_GHC -Wno-unused-imports #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Algorithm.Diff@@ -8,12 +13,55 @@ -- Portability : portable -- -- This is an implementation of the diff algorithm as described in--- /An \( O(ND) \) Difference Algorithm and Its Variations (1986)/--- <http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.6927>.+-- [/An \( O(ND) \) Difference Algorithm and Its Variations (1986)/+-- by Eugene W. Myers](https://publications.mpi-cbg.de/Myers_1986_6330.pdf). -- For inputs of size \( O(N) \) with the number of differences \( D \) -- it has \( O(ND) \) time and \( O(D^2) \) space complexity.+--+-- == Algorithm overview+--+-- Finding the shortest edit script (SES) from a list \( as \) to a list \( bs \)+-- is modelled as a shortest-path search on an /edit graph/: an+-- \( (M+1) \times (N+1) \) grid of nodes \( (i, j) \),+-- where \( M \) and \( N \) are the lengths of \( as \) and \( bs \) respectively,+-- with \( i \) increasing rightward and \( j \) increasing downward.+-- Each node represents the state of having consumed \( i \) elements of \( as \)+-- and \( j \) elements of \( bs \). Three types of move are possible:+--+-- * A /rightward/ move \( (i,j) \to (i+1,j) \) represents+-- /deleting/ \( as[i] \) and costs one edit.+-- * A /downward/ move \( (i,j) \to (i,j+1) \) represents+-- /inserting/ \( bs[j] \) and costs one edit.+-- * A /diagonal/ move \( (i,j) \to (i+1,j+1) \) is free (zero edit cost)+-- and is only available when \( as[i] = bs[j] \).+--+-- The SES corresponds to a path from \( (0,0) \) to \( (M,N) \) that minimises+-- the number of non-diagonal moves.+--+-- Both input lists are 0-indexed, which leads to a slightly different+-- interpretation of the edit graph than in the original paper. In the paper,+-- each node represents the state of the traversal /after/ an edit, so a move+-- is the edit that /produced/ that node. Here, each node represents the state+-- /before/ an edit, so a move is the edit performed /on/ that node to yield its+-- successor. This distinction is only relevant when reading the implementation+-- alongside the paper.+--+-- === K-diagonals and the wave front+--+-- Every node \( (i,j) \) lies on the /k-diagonal/ \( k = i - j \).+-- After exactly \( D \) non-diagonal moves, every reachable node lies on one of+-- at most \( D+1 \) k-diagonals \( k \in \{-D,\,-D+2,\,\ldots,\,D-2,\,D\} \).+-- On each diagonal it suffices to track only the /furthest-reaching/ node+-- (the one with the largest \( i \)), collapsing the two-dimensional grid to a+-- one-dimensional /wave front/ indexed by \( k \).+--+-- The algorithm performs a breadth-first search over \( D = 0, 1, 2, \ldots \),+-- advancing the wave front by one edit at a time until a node reaches the goal+-- \( (M, N) \). The edit trace stored in that node is the SES, which+-- 'getDiffBy' reconstructs into a 'PolyDiff' list. The term /trace/ here+-- differs from the paper, where it denotes the sequence of k-diagonals visited+-- by the SES path; that structure is not materialised in this implementation. ------------------------------------------------------------------------------ module Data.Algorithm.Diff ( Diff, PolyDiff(..) -- * Comparing lists for differences@@ -27,68 +75,292 @@ import Prelude hiding (pi) import Data.Array (listArray, (!))-import Data.Bifunctor+import Data.Algorithm.Diff.Type+import Data.Algorithm.Diff.Refinement (fst3, snd3, thd3, headIsFirst,+ headIsSecond, headIsBoth, noStuttering)+import Data.Foldable (find) +-- | /Diff Instruction/ — an internal enum recording the direction of a single+-- non-diagonal edge traversed in the Myers edit graph. Every non-diagonal+-- move in the edit script is one of:+--+-- * 'F' — /First/ — a horizontal edge \( (i,j) \to (i+1,j) \), which+-- corresponds to /deleting/ the element at position \( i \) of the first input+-- sequence. The consumed element appears in the 'First' branch of the+-- resulting 'PolyDiff'.+--+-- * 'S' — /Second/ — a vertical edge \( (i,j) \to (i,j+1) \), which+-- corresponds to /inserting/ the element at position \( j \) of the second+-- input sequence. The consumed element appears in the 'Second' branch of+-- the resulting 'PolyDiff'.+--+-- Diagonal edges (free moves corresponding to equal elements) are /not/+-- recorded as 'DI' steps; they are followed implicitly by 'addsnake' and+-- produce 'Both' entries in the final output. data DI = F | S deriving (Show, Eq) --- | A value is either from the 'First' list, the 'Second' or from 'Both'.--- 'Both' contains both the left and right values, in case you are using a form--- of equality that doesn't check all data (for example, if you are using a--- newtype to only perform equality on side of a tuple).-data PolyDiff a b = First a | Second b | Both a b- deriving (Show, Eq)--instance Functor (PolyDiff a) where- fmap _ (First a) = First a- fmap g (Second b) = Second (g b)- fmap g (Both a b) = Both a (g b)--instance Bifunctor PolyDiff where- bimap f _ (First a) = First (f a)- bimap _ g (Second b) = Second (g b)- bimap f g (Both a b) = Both (f a) (g b)+-- | /D-path Location/ — a node on the wave front of the Myers O(ND) diff+-- algorithm.+--+-- Each wave front consists of one 'DL' per /k-diagonal/. A 'DL' stores the+-- endpoint coordinates and the edit trace of a \( D \)-path, i.e. a path from the+-- origin \( (0,0) \) that uses exactly \( D \) non-diagonal edges.+{-@+data DL = DL+ { poi :: Nat+ , poj :: Nat+ , path :: { p : [DI] | len p <= poi + poj }+ }+@-}+data DL = DL+ { poi :: !Int -- ^ /Position On I/ — the @x@-coordinate of the endpoint+ -- in the edit graph, i.e. the number of elements+ -- consumed from the /first/ input sequence so far.+ , poj :: !Int -- ^ /Position On J/ — the @y@-coordinate of the endpoint+ -- in the edit graph, i.e. the number of elements+ -- consumed from the /second/ input sequence so far.+ , path :: [DI] -- ^ The edit trace accumulated so far, stored in+ -- /reverse/ order (most recent step first). Diagonal+ -- edges (matches) are not recorded here; only 'F' and+ -- 'S' steps are stored.+ } deriving (Show, Eq) --- | This is 'PolyDiff' specialized so both sides are the same type.-type Diff a = PolyDiff a a+{-@ reflect furthestReaching @-}+-- | Select the furthest-reaching candidate of two 'DL' nodes competing for the+-- same k-diagonal, as required by the Myers algorithm.+--+-- The candidate that has advanced further along the \( x \)-axis (larger 'poi')+-- is the furthest-reaching endpoint on that diagonal.+--+-- Precondition: arguments @x@ and @y@ in @furthestReaching x y@ are in the+-- same /k-diagonal/, meaning that+--+-- > poi x - poj x == poi y - poj y`+--+-- and both argument nodes are within the same wave front,+--+-- > length (path x) == length (path y)+{-@ furthestReaching+ :: x : DL+ -> {y : DL | _kdiag x = _kdiag y && len (path x) = len (path y)}+ -> DL+ @-}+furthestReaching :: DL -> DL -> DL+furthestReaching x y+ | poi x >= poi y = x+ | otherwise = y -data DL = DL {poi :: !Int, poj :: !Int, path::[DI]} deriving (Show, Eq)+-- | Build a /diagonal predicate/ — a closure that tests whether position+-- @(i, j)@ in the edit graph has a diagonal edge (a /match point/ in Myers'+-- terminology).+--+-- Indices are 0-based (\( i \in [0, lena) \), \( j \in [0, lenb) \) ),+-- unlike the 1-based convention of the original paper.+--+-- The first two 'Int' parameters stand for the lengths of the input lists,+-- which are captured from the outer scope to compute them only once.+{-@+canDiag :: (a -> b -> Bool)+ -> [a]+ -> [b]+ -> lena : Int+ -> lenb : Int+ -> DiagPred lena lenb+@-}+canDiag :: (a -> b -> Bool) -- ^ Custom equality predicate+ -> [a] -- ^ First input+ -> [b] -- ^ Second input+ -> Int -- ^ First input's length+ -> Int -- ^ Second input's lenth+ -> (Int -> Int -> Bool) -- ^ Diagonal predicate on the edit grid+canDiag eq as bs lena lenb = \i j ->+ (i < lena && j < lenb) && ((arAs ! i) `eq` (arBs ! j))+ where+ -- Lists are converted into arrays to have O(1) lookups.+ arAs = listArray (0,lena - 1) as+ arBs = listArray (0,lenb - 1) bs -instance Ord DL- where x <= y = if poi x == poi y- then poj x > poj y- else poi x <= poi y+{-@ reflect hStep @-}+hStep :: DL -> DL+hStep node = node {poi = poi node + 1, path = F : path node} -canDiag :: (a -> b -> Bool) -> [a] -> [b] -> Int -> Int -> Int -> Int -> Bool-canDiag eq as bs lena lenb = \ i j ->- if i < lena && j < lenb then (arAs ! i) `eq` (arBs ! j) else False- where arAs = listArray (0,lena - 1) as- arBs = listArray (0,lenb - 1) bs+{-@ reflect vStep @-}+vStep :: DL -> DL+vStep node = node {poj = poj node + 1, path = S : path node} -dstep :: (Int -> Int -> Bool) -> [DL] -> [DL]-dstep cd dls = hd:pairMaxes rst- where (hd:rst) = nextDLs dls- nextDLs [] = []- nextDLs (dl:rest) = dl':dl'':nextDLs rest- where dl' = addsnake cd $ dl {poi=poi dl + 1, path=(F : pdl)}- dl'' = addsnake cd $ dl {poj=poj dl + 1, path=(S : pdl)}- pdl = path dl- pairMaxes [] = []- pairMaxes [x] = [x]- pairMaxes (x:y:rest) = max x y:pairMaxes rest+-- | Perform one breadth-first search expansion step, advancing every wave front+-- 'DL' node by one 'DI' edit (one non-diagonal edge) and then following+-- any available snake.+--+-- For each node the 'dstep' produces two candidate successors by adding:+--+-- * An 'F' (delete) move: 'poi' incremented by 1.+-- * An 'S' (insert) move: 'poj' incremented by 1.+--+-- The resulting candidates are merged pairwise: the vertical successor of each+-- node is paired with the horizontal successor of the next node in the wave+-- front. The 'furthestReaching' between them is extended along the available+-- sequence of matching elements using 'addsnake'.+-- When this function is iterated from a single-node seed (as in 'ses'),+-- each such pair always lies on the same diagonal: an 'F' edge advances to the+-- 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 a non-empty @WaveFront@.+--+-- Postcondition: The node list must be a non-empty @WaveFront@+-- with one more node than the input.+{-@+dstep+ :: lena : Nat+ -> lenb : Nat+ -> DiagPred lena lenb+ -> d : Nat+ -> {nodes : WaveFront lena lenb d | len nodes > 0+ && not (endPoint lena lenb (head nodes))+ && _wfDistanceToGoal lena lenb nodes > 0}+ -> {v : WaveFront lena lenb (d + 1) | len v > 0 && _reducesDistanceToGoal lena lenb nodes v}+@-}+dstep+ :: Int -- ^ First input's length phantom parameter for termination check.+ -> Int -- ^ Second input's length phantom parameter for termination check.+ -> (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+-- @lena@, @lenb@ and @_d@ are named in the first equation as a workaround+-- to https://github.com/ucsd-progsys/liquidhaskell/issues/2704+dstep lena lenb _ _d [] = error "dstep: Cannot perform expansion on an empty list of nodes"+-- This definition branches according to whether a node is on a boundary+-- to avoid constructing out-of-bound nodes and discarding other non-competing nodes.+dstep lena lenb cd _ (dl:dls) =+ if poi dl >= lena then stepAndMerge dl dls+ else+ (addsnake lena lenb cd (hStep dl) : stepAndMerge dl dls)+ -- If @dl@ lies on the bottom boundary, @stepAndMerge dl dls@ discards+ -- all of @dls@; the lemma shows the discarded nodes are farther from+ -- the goal than @dl@'s horizontal child.+ `const` _wfDistanceLowerBound lena lenb dl dls+ where+ -- 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 lena lenb _d+ -> nodes : {xs : [DLN lena lenb _d] | _wfDiags (_kdiag prev - 2) xs+ && _wfDistanceToGoal lena lenb xs > 0}+ -> {v : [DLN lena lenb (_d + 1)]+ | _wfDiags (_kdiag prev - 1) v+ && (poj prev < lenb <=> len v > 0)+ && (len v > 0 => _kdiag (head v) == _kdiag prev - 1)+ && (len v > 0 =>+ _wfDistanceToGoal lena lenb v < _manhattanDistance lena lenb prev)+ && (len v > 0 =>+ _wfDistanceToGoal lena lenb v < _wfDistanceToGoal lena lenb nodes)+ }+ / [len nodes] @-}+ stepAndMerge prev nodes =+ -- When a node lies in the bottom boundary no subsequent node can reach+ -- the goal faster. See lemma '_wfDistanceLowerBound'.+ if poj prev >= lenb then []+ else case nodes of+ [] -> [addsnake lena lenb cd $ vStep prev]+ (next:rest) ->+ -- The next node being on the right border implies 'hStep' would+ -- produce a node outside the grid, but also that previous node's+ -- children cannot compete to the endpoint.+ -- However, we keep @prev@'s vertical child node to preserve+ -- the '_wfDiags' invariant at a negligible performance penalty.+ -- See [NOTE: diagonal-invariant]+ if poi next >= lena then vStep prev : stepAndMerge next rest+ else+ (addsnake lena lenb cd (furthestReaching (vStep prev) (hStep next)) : stepAndMerge next rest)+ -- If @next@ lies on the bottom boundary, the recursive call+ -- discards all of @rest@; the lemma shows the discarded nodes+ -- are farther from the goal than the merged child.+ `const` _wfDistanceLowerBound lena lenb next rest -addsnake :: (Int -> Int -> Bool) -> DL -> DL-addsnake cd dl- | cd pi pj = addsnake cd $+-- | Follow a /snake/ from the current position of a 'DL' node.+--+-- A snake is a sequence of diagonal (cost-free) edges in the edit graph,+-- i.e. a run of equal elements that can be consumed simultaneously+-- from both input sequences without counting as an edit. Starting from+-- @(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 :: lena : Nat+ -> lenb : Nat+ -> DiagPred lena lenb+ -> {dl : DL | _withinBounds lena lenb dl}+ -> {v : DL | path v == path dl+ && _kdiag v = _kdiag dl+ && _withinBounds lena lenb v+ && poi v >= poi dl+ && poj v >= poj dl}+ / [_manhattanDistance lena lenb dl]+@-}+addsnake :: Int -- ^ First input's length phantom parameter for termination check.+ -> Int -- ^ Second input's length phantom parameter for termination check.+ -> (Int -> Int -> Bool) -- ^ Diagonal predicate, a.k.a. 'canDiag'+ -> DL+ -> DL+addsnake lena lenb cd dl+ | cd pi pj = addsnake lena lenb cd $ dl {poi = pi + 1, poj = pj + 1, path = path dl} | otherwise = dl where pi = poi dl; pj = poj dl -lcs :: (a -> b -> Bool) -> [a] -> [b] -> [DI]-lcs eq as bs = path . head . dropWhile (\dl -> poi dl /= lena || poj dl /= lenb) .- concat . iterate (dstep cd) . (:[]) . addsnake cd $- DL {poi=0,poj=0,path=[]}- where cd = canDiag eq as bs lena lenb- lena = length as; lenb = length bs+-- | Compute shortest edit script (SES), as the minimum sequence of 'DI' edit+-- steps that transforms @as@ into @bs@, returned in reverse order.+--+-- @ses eq as bs@ runs the Myers O(ND) diff algorithm:+--+-- 1. __Seed__: create an initial 0-path wave front @[addsnake lena lenb cd (DL 0 0 [])]@+-- having a single node on the tip of the longest origin-sourced snake.+-- 2. __Search__: for each wave front at edit distance \( D = 0, 1, \ldots \),+-- check whether any node has reached the goal @(lena, lenb)@. If not,+-- apply 'dstep' to advance to edit distance \( D+1 \).+-- 3. __Extract__: the first goal node's 'path' field carries the edit+-- trace in reverse order.+--+-- This implementation deviates from the paper in the folowing way:+-- rather than updating a shared diagonal frontier array in place,+-- as in the original paper, it builds a new list of 'DL' nodes+-- for each value of \( D \). This is simpler but carries a+-- larger per-node overhead: each 'DL' holds its own edit trace as a @['DI']@+-- list that structurally shares its tail with the parent node's trace (consing+-- one step reuses the existing spine), rather than the paper's+-- single-integer-per-diagonal representation. The asymptotic time+-- and space complexity — \( O(ND) \) and \( O(D^2) \) respectively — is+-- unchanged.+ses :: (a -> b -> Bool) -> [a] -> [b] -> [DI]+ses eq as bs = path $ searchEndpoint 0 [addsnake lena lenb cd (DL 0 0 [])]+ where+ cd = canDiag eq as bs lena lenb+ lena = length as; lenb = length bs+ {-@ searchEndpoint+ :: d : Nat+ -> {dls : WaveFront lena lenb d | len dls > 0}+ -> {v : DL | endPoint lena lenb v}+ / [_wfDistanceToGoal lena lenb dls] @-}+ searchEndpoint :: Int -> [DL] -> DL+ searchEndpoint _ [] = error "ses: The search must have a seed node"+ searchEndpoint d wf = case findEndpoint lena lenb wf of+ Just p -> p+ Nothing -> let wf' = dstep lena lenb cd d wf+ _lemmaNonNeg = _minDistanceNonNegative lena lenb wf'+ in searchEndpoint (d + 1) wf'+ -- The abstract refinement @q@ lets 'find' carry the wave+ -- front element refinement (notably @len (path dl) == d@)+ -- over to the returned endpoint.+ {-@ assume findEndpoint+ :: forall <q :: DL -> Bool>.+ i : Nat -> j : Nat -> xs : [DL<q>]+ -> { m : Maybe {dl : DL<q> | endPoint i j dl}+ | m == Nothing => _wfDistanceToGoal i j xs > 0} @-}+ findEndpoint :: Int -> Int -> [DL] -> Maybe DL+ findEndpoint i j = find (endPoint i j) -- | Takes two lists and returns a list of differences between them. This is -- 'getDiffBy' with '==' used as predicate.@@ -105,33 +377,287 @@ -- -- > > getGroupedDiff "abcde" "acdf" -- > [Both "a" "a",First "b",Both "cd" "cd",First "e",Second "f"]+{-@ getGroupedDiff :: Eq a => [a] -> [a]+ -> {v:[GroupedDiff a a] | noStuttering v} @-} getGroupedDiff :: (Eq a) => [a] -> [a] -> [Diff [a]] getGroupedDiff = getGroupedDiffBy (==) -- | A form of 'getDiff' with no 'Eq' constraint. Instead, an equality predicate -- is taken as the first argument. getDiffBy :: (a -> b -> Bool) -> [a] -> [b] -> [PolyDiff a b]-getDiffBy eq a b = markup a b . reverse $ lcs eq a b+getDiffBy eq a b = markup a b . reverse $ ses eq a b where markup (x:xs) (y:ys) ds | eq x y = Both x y : markup xs ys ds markup (x:xs) ys (F:ds) = First x : markup xs ys ds markup xs (y:ys) (S:ds) = Second y : markup xs ys ds markup _ _ _ = [] +-- | Like 'getGroupedDiff' but accepts a custom equality predicate.+--+-- Postcondition: the output list is guaranteed to be /chunked/. i.e. no two adjacent+-- elements share the same constructor.+{-@ getGroupedDiffBy :: (a -> b -> Bool) -> [a] -> [b]+ -> {vs : [GroupedDiff a b] | noStuttering vs} @-} getGroupedDiffBy :: (a -> b -> Bool) -> [a] -> [b] -> [PolyDiff [a] [b]]-getGroupedDiffBy eq a b = go $ getDiffBy eq a b- where go (First x : xs) = let (fs, rest) = goFirsts xs in First (x:fs) : go rest- go (Second x : xs) = let (fs, rest) = goSeconds xs in Second (x:fs) : go rest- go (Both x y : xs) = let (fs, rest) = goBoth xs- (fxs, fys) = unzip fs- in Both (x:fxs) (y:fys) : go rest- go [] = []+getGroupedDiffBy eq a b = groupDiff $ getDiffBy eq a b+ where+ {-@ groupDiff :: xs : [PolyDiff a b]+ -> {vs : [GroupedDiff a b] | noStuttering vs+ // The following predicates allow LiquidHaskell keep track+ // of the head constructor in each recursive call.+ && (headIsFirst xs <=> headIsFirst vs)+ && (headIsSecond xs <=> headIsSecond vs)+ && (headIsBoth xs <=> headIsBoth vs)} @-}+ groupDiff :: [PolyDiff a b] -> [PolyDiff [a] [b]]+ groupDiff (First x : xs) = let (fs, rest) = leadingFirsts xs+ in First (x:fs) : groupDiff rest+ groupDiff (Second x : xs) = let (sc, rest) = leadingSeconds xs+ in Second (x:sc) : groupDiff rest+ groupDiff (Both x y : xs) = let (bxs, bys, rest) = leadingBoths xs+ in Both (x:bxs) (y:bys) : groupDiff rest+ groupDiff [] = [] - goFirsts (First x : xs) = let (fs, rest) = goFirsts xs in (x:fs, rest)- goFirsts xs = ([],xs)+ {-@ leadingFirsts :: xs : [PolyDiff a b]+ -> {v : ([a], [PolyDiff a b])+ | not (headIsFirst (snd v))+ // Here, and in the analogous helpers,+ // the length comparison is needed for termination check.+ && len (snd v) <= len xs+ && (headIsSecond xs => headIsSecond (snd v))+ && (headIsBoth xs => headIsBoth (snd v))} @-}+ leadingFirsts :: [PolyDiff a b] -> ([a], [PolyDiff a b])+ leadingFirsts (First y : diffs) = let (firsts, rest) = leadingFirsts diffs+ in (y:firsts, rest)+ leadingFirsts diffs = ([],diffs) - goSeconds (Second x : xs) = let (fs, rest) = goSeconds xs in (x:fs, rest)- goSeconds xs = ([],xs)+ {-@ leadingSeconds :: xs : [PolyDiff a b]+ -> {v : ([b], [PolyDiff a b])+ | not (headIsSecond (snd v))+ && len (snd v) <= len xs+ && (headIsFirst xs => headIsFirst (snd v))+ && (headIsBoth xs => headIsBoth (snd v))} @-}+ leadingSeconds :: [PolyDiff a b] -> ([b], [PolyDiff a b])+ leadingSeconds (Second y : diffs) = let (seconds, rest) = leadingSeconds diffs+ in (y:seconds, rest)+ leadingSeconds diffs = ([],diffs) - goBoth (Both x y : xs) = let (fs, rest) = goBoth xs in ((x,y):fs, rest)- goBoth xs = ([],xs)+ {-@ leadingBoths :: xs : [PolyDiff a b]+ -> {v : ([a], [b], [PolyDiff a b])+ | not (headIsBoth (thd3 v))+ && len (thd3 v) <= len xs+ && (headIsFirst xs => headIsFirst (thd3 v))+ && (headIsSecond xs => headIsSecond (thd3 v))+ && len (fst3 v) == len (snd3 v)} @-}+ leadingBoths :: [PolyDiff a b] -> ([a], [b], [PolyDiff a b])+ leadingBoths (Both w z : diffs) = let (as, bs, rest) = leadingBoths diffs+ in (w:as, z:bs, rest)+ leadingBoths diffs = ([], [], diffs)++--------------------------------------------------------------------------------+-- * LiquidHaskell Wave Front Specification+--+-- Wave fronts establish a connection between the orignal the Myers algorithm+-- and this implementation:+-- Their nodes carry the edit distance, which also corresponds to the+-- algorithm's current iteration step and the resulting 'ses' length.+-- In Myers the diagonal arrangement invariant of the iteration is used to+-- optimize space; within 'dstep' it allows us to ensure 'furthestReaching'+-- always compares nodes on the same diagonals.+--------------------------------------------------------------------------------++-- Field refinements are implemented with measures, which means they are+-- available only when a 'DL' value is pattern matched;+-- This invariant on DLs makes the coordinates non-negativity available+-- for any value of type 'DL' regardless of whether it has been pattern matched.+{-@ using (DL) as { dl : DL | poi dl >= 0 && poj dl >= 0 } @-}++-- A "D-path location node" is a 'DL' value within the edit grid bounds+-- having a fixed /D-length/.+{-@ type DLN M N D = { x : DL | len (path x) = D && _withinBounds M N x} @-}++{-@ reflect _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.+-- See [NOTE: diagonal-invariant]+_wfDiags :: Int -> [DL] -> Bool+_wfDiags _ [] = True+_wfDiags k (dl:dls) = _kdiag dl == k && _wfDiags (k - 2) dls++--------------------------------------------------------------------------------+-- [NOTE: diagonal-invariant]+--+-- The '_wfDiags' predicate states that succesive nodes in a wave front lie+-- on diagonals whose indices differ by two. This is leveraged by LiquidHaskell+-- to check that the 'furthestReaching' precondition stating that the two nodes+-- it compares lie on the same diagonal is satisfied within `dstep`.+-- However, even though a more flexible predicate could be used to prove it,+-- a compromise was made in preserving this invariant to keep the specification+-- complexity low at a negligible performance penalty cost.+-- This note documents this compromise.+--+-- To prove 'ses' terminates, wave fronts are restricted to be within the+-- edit grid. This is done by placing checks for boundary nodes within 'dstep'+-- to avoid constructing nodes outside the grid. 'dstep' leverages such checks+-- in optimizations that rely on the observation that boundary nodes signal+-- other nodes cannot compete to the goal:+--+-- * If a bottom boundary is found, all subsequent nodes are not considered.+--+-- * If a right boundary is found, all previously constructed child nodes+-- can be dropped.+--+-- Both preserve the diagonal invariant, as the wave front would just become+-- narrower. However, due to the asymmetry of list traversal, the first one is+-- readily implemented, while the second requires an additional operation whose+-- cost trumps the gain of not keeping them for next iterations (according to the+-- existing benchmarks). Because of this, and 'stepAndMege' looking a two+-- succesive nodes at a time, only the current iteration child /could/ be+-- effectively dropped.+--+-- However, dropping the current iteration child node results in wave fronts+-- with holes: now for every right boundary node found, a diagonal is not+-- occupied. This requires the diagonal invariant to be changed to "diagonal+-- indices in succesive nodes of a wave front differ by 2, unless a node lies+-- on the right boundary, in which case its diagonal must differ from the previous+-- by a factor of 2". It was decided to not follow this path, because the gain+-- of not keeping this node was found to be negligible compared with the resulting+-- increase in specification complexity.+--------------------------------------------------------------------------------++-- 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@.+-- See [NOTE: diagonal-invariant]+{-@ type WaveFront M N D = {xs : [DLN M N D] | _wfDiags (_kdiag (head xs)) xs} @-}++--------------------------------------------------------------------------------+-- * Proving the Algorithm's Termination in LiquidHaskell+--+-- The `ses` (_smallest edit script_) function termination is proved by defining+-- a wave front's distance to the _endpoint_ as decreasing metric.+-- This function is the implementation's entry point to the Myers diff algorithm,+-- whose original specification waives the need for a termination proof by+-- bounding the algorithm's outer loop by the known worst case edit script length,+-- i.e. the sum of both input's lengths. These lengths are threaded through the+-- implementation as phantom parameters for the following helpers to provide the+-- LiquidHaskell specification a notion of the edit grid (as nodes '_withinBounds')+-- and its end point.+--------------------------------------------------------------------------------++{-@ reflect _manhattanDistance @-}+_manhattanDistance :: Int -> Int -> DL -> Int+_manhattanDistance lena lenb dl = lena - (poi dl) + lenb - (poj dl)++{-@ reflect _wfDistanceToGoal @-}+-- | The smallest manhattan distance from a wave front node to the goal @(lena, lenb)@.+-- The empty wave front yields @lena + lenb + 2@, a sentinel strictly greater+-- than any in-bounds node's distance, acting as the identity for the minimum.+_wfDistanceToGoal :: Int -> Int -> [DL] -> Int+_wfDistanceToGoal lena lenb [] = lena + lenb + 2+_wfDistanceToGoal lena lenb (dl:dls) =+ -- We avoid using 'min' here so that LH can unfold this definition.+ if _manhattanDistance lena lenb dl < _wfDistanceToGoal lena lenb dls+ then _manhattanDistance lena lenb dl+ else _wfDistanceToGoal lena lenb dls++{-@ inline _reducesDistanceToGoal @-}+_reducesDistanceToGoal :: Int -> Int -> [DL] -> [DL] -> Bool+_reducesDistanceToGoal lena lenb wf1 wf2 =+ _wfDistanceToGoal lena lenb wf2 < _wfDistanceToGoal lena lenb wf1++{-@ inline _withinBounds @-}+{-@ _withinBounds :: lena : Nat -> lenb : Nat -> dl : DL+ -> {v:Bool | v <=> (poi dl <= lena && poj dl <= lenb) } @-}+_withinBounds :: Int -> Int -> DL -> Bool+_withinBounds lena lenb dl = poi dl <= lena && poj dl <= lenb++{-@ inline endPoint @-}+endPoint :: Int -> Int -> DL -> Bool+endPoint lena lenb dl = poi dl == lena && poj dl == lenb++-- This refinement type alias allows LiquidHaskell to reason about the function+-- parameter of 'addsnake' that establishes whether coordinates are within bounds.+{-@ type DiagPred M N = i : Nat -> j : Nat -> {b : Bool | b => i < M && j < N} @-}++-- | A lemma that expresses a lower bound of the wavefront distance in terms+-- of the diagonal of the first node: @lena - lenb - k@+--+-- We assume all the nodes to be within the grid.+--+-- @lena - lenb@ is the diagonal of the goal. Informally, the+-- shortest way from a node must necessarily visit all the intermediate+-- diagonals. The minimum amount of diagonals to visit is given by the+-- difference between the diagonal indices of the goal and the first element.+--+-- We can prove it manually like so:+--+-- For every node @dl = DL i j p@ we can prove+-- @H(dl) = _manhattanDistance lena lenb dl >= lena - lenb - (i - j)@+--+-- @+-- _manhattanDistance lena lenb dl+-- =+-- lena - (poi dl) + lenb - (poj dl)+-- =+-- lena - i + lenb - j+-- =+-- lena - lenb - (i - j) + 2 * (lenb - j)+-- >=+-- lena - lenb - (i - j)+-- @+--+-- Since @H(dl)@ holds for every node in the wave front, it follows+-- that the wave front distance is at least as large as the smallest of+-- these bounds, which is @lena - lenb - k@ for the largest @k = i0 - j0@,+-- which is the diagonal of the first node.+--+-- QED+-- @+{-@ _wfDistanceLowerBoundK+ :: lena : Nat -> lenb : Nat -> {k : Int | lenb + k + 2 >= 0}+ -> xs : {v : [{dl : DL | _withinBounds lena lenb dl}] | _wfDiags k v}+ -> {_wfDistanceToGoal lena lenb xs >= lena - lenb - k}+ / [len xs] @-}+_wfDistanceLowerBoundK :: Int -> Int -> Int -> [DL] -> ()+_wfDistanceLowerBoundK _ _ _ [] = ()+_wfDistanceLowerBoundK lena lenb k (_:dls) = _wfDistanceLowerBoundK lena lenb (k - 2) dls++-- | If a wave front's node (@prev@) is on the bottom boundary, then the following+-- nodes lie farther from the goal. Intuitively, the reason is that the following+-- nodes children would need more steps to cross @prev@'s diagonal to reach the goal.+-- This lemma allows LH to reason about the case where nodes are discarded+-- after a bottom-boundary node within 'dstep'.+{-@+_wfDistanceLowerBound+ :: lena : Nat -> lenb : Nat -> {prev : DL | _withinBounds lena lenb prev}+ -> xs : {v : [{dl : DL | _withinBounds lena lenb dl}] | _wfDiags (_kdiag prev - 2) v}+ -> { poj prev >= lenb => _wfDistanceToGoal lena lenb xs > _manhattanDistance lena lenb prev}+ @-}+_wfDistanceLowerBound :: Int -> Int -> DL -> [DL] -> ()+_wfDistanceLowerBound lena lenb prev [] = ()+_wfDistanceLowerBound lena lenb prev xs@(_:_) = ()+ where+ _lemma = _wfDistanceLowerBoundK lena lenb (_kdiag prev - 2) xs+++-- | The termination metric is non-negative: every in-bounds node has a+-- non-negative manhattan distance to the goal, and the empty wave front+-- yields the positive sentinel. This lemma is needed because the @Nat@ result+-- refinement of the reflected '_wfDistanceToGoal' is not instantiated at+-- logic-level applications, while termination metrics must be provably+-- non-negative.+{-@ _minDistanceNonNegative+ :: lena : Nat -> lenb : Nat+ -> xs : [{dl : DL | _withinBounds lena lenb dl}]+ -> {_wfDistanceToGoal lena lenb xs >= 0}+ / [len xs] @-}+_minDistanceNonNegative :: Int -> Int -> [DL] -> ()+_minDistanceNonNegative _ _ [] = ()+_minDistanceNonNegative lena lenb (_:dls) = _minDistanceNonNegative lena lenb dls
+ src/Data/Algorithm/Diff/Refinement.hs view
@@ -0,0 +1,93 @@+-- | Refinement type aliases for 'PolyDiff', related predicates and (lifted) utility functions.+-- The contents of this module are intended for use in LiquidHaskell specifications;+-- importing this module can result in unused import warnings in GHC,+-- which can be suppressed with @-Wno-unused-imports@.+module Data.Algorithm.Diff.Refinement where++import Data.Algorithm.Diff.Type++-- * Diff predicates and refinement type aliases++{-@+inline validListDiff+define length x = len x+@-}+-- | True when, for a 'Both' value, both sides have the same length.+-- 'First' and 'Second' trivially satisfy this.+validListDiff :: PolyDiff [a] [b] -> Bool+validListDiff (Both xs ys) = length xs == length ys+validListDiff (First _) = True+validListDiff (Second _) = True++{-@ inline nonEmptyDiff @-}+-- | True when the diff is not empty on either side.+nonEmptyDiff :: PolyDiff [a] [b] -> Bool+nonEmptyDiff (First []) = False+nonEmptyDiff (Second []) = False+nonEmptyDiff (Both [] _) = False+nonEmptyDiff (Both _ []) = False+nonEmptyDiff _ = True++-- A valid list diff is such that any `Both` value has arguments of equal length.+{-@ type ValidListDiff a b = { d : PolyDiff [a] [b] | validListDiff d }@-}++-- Non-empty valued valid list diffs, used for grouped diffs.+{-@ type GroupedDiff a b = { d : ValidListDiff a b | nonEmptyDiff d } @-}++{-@ reflect headIsFirst @-}+{-@ reflect headIsSecond @-}+{-@ reflect headIsBoth @-}+-- | Head-constructor predicates for 'PolyDiff' lists.+-- Reflected (not measures) to avoid sort errors: measures on @[PolyDiff a b]@+-- would be attached to the polymorphic @[]@ constructor, clashing with+-- lists of other element types.+headIsFirst, headIsSecond, headIsBoth :: [PolyDiff a b] -> Bool+headIsFirst (First _ : _) = True+headIsFirst _ = False+headIsSecond (Second _ : _) = True+headIsSecond _ = False+headIsBoth (Both _ _ : _) = True+headIsBoth _ = False++{-@ reflect noStuttering @-}+-- | True if the list does not contain adjacent 'Diff's of the same type.+-- Uses head-constructor measures so PLE can work with opaque tails.+noStuttering :: [PolyDiff a b] -> Bool+noStuttering [] = True+noStuttering (First _ : xs) = not (headIsFirst xs) && noStuttering xs+noStuttering (Second _ : xs) = not (headIsSecond xs) && noStuttering xs+noStuttering (Both _ _ : xs) = not (headIsBoth xs) && noStuttering xs++{-@ reflect noFFSS @-}+-- | Like 'noStuttering' but allows Both-Both adjacencies.+-- This is the invariant preserved by @doPrefix@\/@doSuffix@ which may split+-- a single 'Both' into two consecutive 'Both' elements.+noFFSS :: [PolyDiff a b] -> Bool+noFFSS [] = True+noFFSS (First _ : xs) = not (headIsFirst xs) && noFFSS xs+noFFSS (Second _ : xs) = not (headIsSecond xs) && noFFSS xs+noFFSS (Both _ _ : xs) = noFFSS xs++-- 'Diff' type for the precondition of 'diffToLineRanges'.+{-@ type LineDiff = Diff (NonEmpty String) @-}++-- * Lifted utility functions and specification helpers++-- Non-empty lists as refinements of regular lists.+{-@ type NonEmpty a = {xs : [a] | len xs >0}@-}++-- Indices for line numbers.+{-@ type Nat1 = {n : Int | n >= 1 } @-}++-- | Measures for triplet projections.+{-@+measure fst3+measure snd3+measure thd3+@-}+fst3 :: (a, b, c) -> a+fst3 (x, _, _) = x+snd3 :: (a, b, c) -> b+snd3 (_, y, _) = y+thd3 :: (a, b, c) -> c+thd3 (_, _, z) = z
+ src/Data/Algorithm/Diff/Type.hs view
@@ -0,0 +1,33 @@+-- | Basic diff type and instances.+module Data.Algorithm.Diff.Type where++import Data.Bifunctor++-- | A value tagged with which of two input sequences it came from.+-- The type parameters @a@ and @b@ may differ, which is useful when comparing+-- sequences of different element types via a custom equality predicate.+--+-- Each constructor corresponds to one outcome for a position in the aligned+-- sequences:+--+-- * 'First' — the element exists only in the /first/ input (a deletion).+-- * 'Second' — the element exists only in the /second/ input (an insertion).+-- * 'Both' — the element is common to both inputs.+-- Both the left and right values are retained so that the original+-- elements can be recovered even when equality ignores some fields.+{-@ data PolyDiff a b = First a | Second b | Both a b @-}+data PolyDiff a b = First a | Second b | Both a b+ deriving (Show, Eq)++instance Functor (PolyDiff a) where+ fmap _ (First a) = First a+ fmap g (Second b) = Second (g b)+ fmap g (Both a b) = Both a (g b)++instance Bifunctor PolyDiff where+ bimap f _ (First a) = First (f a)+ bimap _ g (Second b) = Second (g b)+ bimap f g (Both a b) = Both (f a) (g b)++-- | This is 'PolyDiff' specialized so both sides are the same type.+type Diff a = PolyDiff a a
src/Data/Algorithm/DiffContext.hs view
@@ -1,3 +1,9 @@+{-@ LIQUID "--ple" @-}+{-@ LIQUID "--ple-with-undecided-guards" @-}+-- Import of the 'Data.Algorithm.Diff.Refinement' module is required for the+-- LiquidHaskell specifications in this module, but is unused in the actual code.+-- The following GHC option suppresses the unused import warning.+{-# OPTIONS_GHC -Wno-unused-imports #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Algorithm.DiffContext@@ -8,7 +14,7 @@ -- Portability : portable -- Author : David Fox (ddssff at the email service from google) ----- Generates a grouped diff with merged runs, and outputs them in the manner of diff -u+-- Generates a grouped diff with merged runs, and outputs them in the manner of @diff -u@. ----------------------------------------------------------------------------- module Data.Algorithm.DiffContext ( ContextDiff, Hunk@@ -18,40 +24,61 @@ , getContextDiffNumbered , Numbered(Numbered), numbered, unnumber , unNumberContextDiff- , groupBy' ) where import Data.Algorithm.Diff (PolyDiff(..), Diff, getGroupedDiff)--- import Data.List (groupBy)+import Data.Algorithm.Diff.Refinement (noStuttering, noFFSS, headIsFirst, headIsSecond) import Data.Bifunctor import Text.PrettyPrint (Doc, text, empty, hcat) +{-@ type ContextDiff c = [Hunk c] @-}+-- | A diff consisting of disjoint 'Hunk's. type ContextDiff c = [Hunk c]-type Hunk c = [Diff [c]] --- | A version of 'groupBy' that does not assume the argument function--- is transitive. This is used to partition the 'Diff' list into--- segments that begin and end with matching ('Both') text, with and--- have non-matching ('First' and 'Second') text in the middle.------ > let notBoth1 a b = not (a == 1 || b == 1) in--- >--- > groupBy' notBoth1 [1,1,2,3,1,1,4,5,6,1]--- > [[1],[1,2,3,1],[1,4,5,6,1]]--- >--- > groupBy notBoth1 [1,1,2,3,1,1,4,5,6,1]--- > [[1],[1,2,3],[1],[1,4,5,6],[1]]+{-@ type Hunk c = { h : [ValidListDiff c c] | noStuttering h} @-}+-- | A 'Hunk' is a list of adjacent 'Diff's. ----- In the first result the list is split anywhere there are two--- adjacent ones, as desired.-groupBy' :: (a -> a -> Bool) -> [a] -> [[a]]-groupBy' _ [] = []-groupBy' eq (x0 : xs0) = go [x0] xs0- where- go (x : xs) (y : zs) | eq x y = go (y : x : xs) zs- go g (y : zs) = reverse g : go [y] zs- go g [] = [reverse g]+-- No two consecutive elements in a 'Hunk' are both applications+-- of 'First', 'Second', or 'Both', i.e. the list does not stutter+-- on 'Diff' constructors.+type Hunk c = [Diff [c]] +-- | Split a 'Diff' list at consecutive 'Both'-'Both' boundaries.+{-@ splitBothBoth :: {ds : [ValidListDiff c c] | noFFSS ds} -> [Hunk c] @-}+splitBothBoth :: [Diff [c]] -> [Hunk c]+splitBothBoth = go []+ where+ {-@ go+ :: g:Hunk c+ -> {xs : [ValidListDiff c c] | noFFSS xs && not (headAlike g xs) }+ -> [Hunk c] / [len xs]+ @-}+ go :: Hunk c -> [Diff [c]] -> [Hunk c]+ go g (x@Both{} : y@Both{} : xs) = reverse (x:g) : go [] (y:xs)+ where+ lemma = lemmaReverseStuttering (x:g)+ go g (x : xs) = go (x:g) xs+ go g [] = [reverse g]+ where+ lemma = lemmaReverseStuttering g++{-@ type ContextSize = Nat @-}+type ContextSize = Int++{-@ opaque-reflect reverse @-}++{-@ assume lemmaReverseStuttering+ :: xs:_ -> { noStuttering (reverse xs) = noStuttering xs } @-}+lemmaReverseStuttering :: Hunk c -> ()+lemmaReverseStuttering _ = ()++{-@ reflect headAlike @-}+headAlike :: Hunk c -> Hunk c -> Bool+headAlike (Both{} : _) (Both{} : _) = True+headAlike (First{} : _) (First{} : _) = True+headAlike (Second{} : _) (Second{} : _) = True+headAlike _ _ = False+ data Numbered a = Numbered Int a deriving Show instance Eq a => Eq (Numbered a) where Numbered _ a == Numbered _ b = a == b@@ -81,48 +108,110 @@ -- > i -- > j -- > -k+{-@ getContextDiff :: Eq a- => Maybe Int -- ^ Number of context elements, Nothing means infinite+ => Maybe ContextSize -> [a] -> [a] -> ContextDiff (Numbered a)-getContextDiff context a b =- getContextDiffNumbered context (numbered a) (numbered b)+@-}+getContextDiff ::+ Eq a+ => Maybe ContextSize -- ^ Context size. 'Nothing' means returning a whole-diff 'Hunk'.+ -> [a]+ -> [a]+ -> ContextDiff (Numbered a)+getContextDiff contextSize a b =+ getContextDiffNumbered contextSize (numbered a) (numbered b) -- | If for some reason you need the line numbers stripped from the--- result of getContextDiff for backwards compatibility.+-- result of 'getContextDiff' for backwards compatibility.+{-@ unNumberContextDiff :: ContextDiff (Numbered a) -> [[Diff [a]]] @-} unNumberContextDiff :: ContextDiff (Numbered a) -> ContextDiff a unNumberContextDiff = fmap (fmap (bimap (fmap unnumber) (fmap unnumber))) +-- | Create a diff of separate 'Hunk's, each containing a sequence+-- of differing elements surrounded by common elements for context.+--+-- The context size determines when to merge adjacent hunks:+-- two hunks are merged when the number of common elements between them does not+-- exceed twice the context size. Furthermore, if @contextSize@ is 'Nothing'+-- a single hunk with the whole diff is produced.+{-@ getContextDiffNumbered :: Eq a- => Maybe Int -- ^ Number of context elements, Nothing means infinite+ => Maybe ContextSize -> [Numbered a] -> [Numbered a] -> ContextDiff (Numbered a)-getContextDiffNumbered context a0 b0 =- groupBy' (\a b -> not (isBoth a && isBoth b)) $ doPrefix $ getGroupedDiff a0 b0+@-}+getContextDiffNumbered ::+ Eq a+ => Maybe ContextSize -- ^ Context size. 'Nothing' means returning a whole-diff 'Hunk'.+ -> [Numbered a]+ -> [Numbered a]+ -> ContextDiff (Numbered a)+getContextDiffNumbered Nothing a0 b0 = [getGroupedDiff a0 b0]+getContextDiffNumbered (Just contextSize) a0 b0 =+ -- The 'Diff' list is grouped into 'Hunks' that begin and end+ -- with matching ('Both') text, having non-matching ('First' and 'Second')+ -- text in the middle. Note that a non-trivial partition can only happen after+ -- the matching text has been reduced to become consecutive 'Both' values+ -- corresponding to a hunk's suffix and the following hunk prefix.+ splitBothBoth $ doPrefix $ getGroupedDiff a0 b0 where- isBoth (Both _ _) = True- isBoth _ = False- -- Handle the common text leading up to a diff.+ -- | Handle the common text leading up to a diff.+ --+ -- Postcondition: The @a@ elements in @doPrefix h@ are a subset of those in @h@,+ -- in the same order. Additionaly, 'First' and 'Second' diffs+ -- are identical in both lists.+ --+ -- The difference between input and output is that some 'Both' diffs might+ -- be split into two other 'Both' diffs. This happens when their contents+ -- are too large compared with the contex size, resulting in some @a@+ -- elements being dropped.+ {-@ doPrefix :: h : Hunk c+ -> {v : [ValidListDiff c c] | noFFSS v+ && (headIsFirst h <=> headIsFirst v)+ && (headIsSecond h <=> headIsSecond v)} / [len h, 0] @-}+ doPrefix :: Hunk c -> [Diff [c]] doPrefix [] = []+ -- Trailing common elements are no prefix.+ -- This case corresponds to when both input lists are identical, so the+ -- resulting 'ContextDiff' is empty. doPrefix [Both _ _] = []+ -- Do the prefix and then make the suffix. doPrefix (Both xs ys : more) =- Both (maybe xs (\n -> drop (max 0 (length xs - n)) xs) context)- (maybe ys (\n -> drop (max 0 (length ys - n)) ys) context) : doSuffix more- -- Prefix finished, do the diff then the following suffix- doPrefix (d : ds) = doSuffix (d : ds)- -- Handle the common text following a diff.+ Both (drop (length xs - contextSize) xs)+ (drop (length ys - contextSize) ys) : doSuffix more+ -- Prefix finished, do the diff then the following suffix.+ doPrefix (d : ds) = d : doSuffix ds++ -- | Handle the common text following a diff.+ --+ -- Precondition: The input does not start with a 'Both' diff. Otherwise,+ -- it behaves like @doPrefix@.+ {-@ doSuffix :: h : Hunk c+ -> {v : [ValidListDiff c c] | noFFSS v+ && (headIsFirst h <=> headIsFirst v)+ && (headIsSecond h <=> headIsSecond v)} / [len h, 1] @-}+ doSuffix :: Hunk c -> [Diff [c]] doSuffix [] = []- doSuffix [Both xs ys] = [Both (maybe xs (\n -> take n xs) context) (maybe ys (\n -> take n ys) context)]+ -- A trailing suffix.+ doSuffix [Both xs ys] = [Both (take contextSize xs) (take contextSize ys)]+ -- If the common text is too short compared with the context,+ -- we preserve it and continue. As the following element cannot be a 'Both'+ -- as well, this effectively places the common text in the inner part of the diff.+ -- Otherwise, we split it into a suffix and prefix+ -- (resulting in some elements excluded from the diff in the middle). doSuffix (Both xs ys : more)- | maybe True (\n -> length xs <= n * 2) context =- Both xs ys : doPrefix more- doSuffix (Both xs ys : more) =- Both (maybe xs (\n -> take n xs) context) (maybe ys (\n -> take n ys) context)- : doPrefix (Both (maybe mempty (\n -> drop n xs) context) (maybe mempty (\n -> drop n ys) context) : more)+ | length xs <= contextSize * 2 =+ Both xs ys : doPrefix more+ | otherwise =+ Both (take contextSize xs) (take contextSize ys) :+ doPrefix (Both (drop contextSize xs) (drop contextSize ys) : more)+ -- 'First' and 'Second' elements are no suffix, preserve them and continue looking. doSuffix (d : ds) = d : doSuffix ds -- | Pretty print a ContextDiff in the manner of diff -u.
src/Data/Algorithm/DiffOutput.hs view
@@ -8,7 +8,7 @@ -- Portability : portable -- Author : Stephan Wehr (wehr@factisresearch.com) and JP Moresmau (jp@moresmau.fr) ----- Generates a string output that is similar to diff normal mode+-- Generates a string output that is similar to diff normal mode. ----------------------------------------------------------------------------- module Data.Algorithm.DiffOutput where import Data.Algorithm.Diff@@ -16,34 +16,59 @@ import Data.Char import Data.List --- | Converts Diffs to DiffOperations+-- | 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 :: [LineDiff] -> [DiffOperation ValidLineRange] @-} 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 :: Nat1+ -> Nat1+ -> diffs : [LineDiff]+ -> [DiffOperation ValidLineRange] / [len diffs, 0] @-} toLineRange :: Int -> Int -> [Diff [String]] -> [DiffOperation LineRange] toLineRange _ _ []=[]+ -- If the lines are the same, we just move forward. toLineRange leftLine rightLine (Both ls _:rs)= let lins=length ls in toLineRange (leftLine+lins) (rightLine+lins) rs- toLineRange leftLine rightLine (Second lsS:First lsF:rs)=+ -- A 'Change' is introduced when an addition is followed by a deletion, or vice versa.+ 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- 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 (First lsF:rs)=- let linesF=length lsF- diff=Deletion (LineRange (leftLine,leftLine+linesF-1) lsF) (rightLine-1)- in diff: toLineRange(leftLine+linesF) rightLine rs+ -- Introduce 'Addition's.+ 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 diff = Deletion (mkLineRange leftLine lsF) (rightLine-1)+ in diff : toLineRange (leftLine + length lsF) rightLine rs+ -- | Build 'Change's from adjacent additions and deletions.+ {-@ toChange :: Nat1+ -> Nat1+ -> NonEmpty String+ -> NonEmpty String+ -> diffs : [LineDiff]+ -> [DiffOperation ValidLineRange]+ / [len diffs, 1] @-}+ toChange :: Int -- ^ Current left line number.+ -> Int -- ^ Current right line number.+ -> [String] -- ^ Lines from the 'First' list (corresponding to deletions).+ -> [String] -- ^ Lines from the 'Second' list (corresponding to additions).+ -> [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 --- | pretty print the differences. The output is similar to the output of the diff utility+{-@ ppDiff :: [LineDiff] -> 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"])) -- > 2d1@@ -59,7 +84,7 @@ render (prettyDiffs diffLineRanges) ++ "\n" --- | pretty print of diff operations+-- | Pretty print of diff operations. prettyDiffs :: [DiffOperation LineRange] -> Doc prettyDiffs [] = empty prettyDiffs (d : rest) = prettyDiff d $$ prettyDiffs rest@@ -80,59 +105,114 @@ prettyLines start lins = vcat (map (\l -> char start <+> text l) lins) --- | Parse pretty printed Diffs as DiffOperations+-- | Parse pretty printed 'Diff's as 'DiffOperation's. parsePrettyDiffs :: String -> [DiffOperation LineRange] parsePrettyDiffs = reverse . doParse [] . lines where- doParse diffs [] = diffs- doParse diffs s =+ -- | Parsing entry point that iteratively accumulates 'DiffOperation's+ -- until the input is exhausted.+ {-@ doParse :: [DiffOperation LineRange] -> diffs : [String] -> [DiffOperation LineRange] / [len diffs] @-}+ doParse :: [DiffOperation LineRange] -> [String] -> [DiffOperation LineRange]+ -- NOTE: Incorrectly formatted lines are ignored.+ doParse acc [] = acc+ doParse acc s = let (mnd,r) = parseDiff s in case mnd of- Just nd -> doParse (nd:diffs) r- _ -> doParse diffs r+ Just nd -> doParse (nd:acc) r+ _ -> doParse acc r++ parseDiff :: [String] -> (Maybe (DiffOperation LineRange), [String]) parseDiff [] = (Nothing,[]) parseDiff (h:rs) = let (r1,hrs1) = parseRange h in case hrs1 of+ -- In each case, we pass the left line range,+ -- the remaining string after the type character,+ -- which must contain the right line range,+ -- and the remaining lines to parse. ('d':hrs2) -> parseDel r1 hrs2 rs ('a':hrs2) -> parseAdd r1 hrs2 rs ('c':hrs2) -> parseChange r1 hrs2 rs _ -> (Nothing,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)++ 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)++ 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) _ -> (Nothing,rs2)+ parseRange :: String -> ((LineNo, LineNo),String) parseRange l = let (fstLine,rs) = span isDigit l (sndLine,rs3) = case rs of+ -- The comma is used to separate+ -- the start and end line numbers in a range,+ -- but is omitted if they are the same.+ -- i.e. the range is a single line. (',':rs2) -> span isDigit rs2 _ -> (fstLine,rs) in ((read fstLine,read sndLine),rs3) --- | Line number alias+-- | Line number alias. Always non-negative. type LineNo = Int --- | Line Range: start, end and contents+-- | Line Range: start, end and contents.+--+-- The following invariants hold:+--+-- > snd lrNumbers >= fst lrNumbers+-- > snd lrNumbers - fst lrNumbers + 1 == length lrContents+--+-- which imply @lrContents@ cannot be empty.+{-@ data LineRange = LineRange { lrNumbers :: (LineNo, LineNo) , lrContents :: [String] }- deriving (Show,Read,Eq,Ord)+@-}+data LineRange = LineRange { lrNumbers :: (LineNo, LineNo)+ , lrContents :: [String]+ }+ deriving (Show, Read, Eq, Ord) --- | Diff Operation representing changes to apply-data DiffOperation a = Deletion a LineNo- | Addition a LineNo- | Change a a- deriving (Show,Read,Eq,Ord)+{-@ predicate validRange Start End ContentLenght = Start >= 0 && End >= 0 && Start <= End && ContentLenght = End - Start + 1 @-}++{-@ type ValidLineRange = {r : LineRange | validRange (fst (lrNumbers r)) (snd (lrNumbers r)) (len (lrContents r))} @-}++-- | 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 :: Nat -> {contents : [String] | len contents >= 1} -> ValidLineRange @-}+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+ -- preceding the deleted lines in the right input.+ | Addition a LineNo -- ^ Element added from the right input, line number+ -- preceding the added lines in the left input.+ | Change a a -- ^ Element changed from the left input to the right input.+ deriving (Show,Read,Eq,Ord)
test/Test.hs view
@@ -11,6 +11,7 @@ import Data.Algorithm.DiffOutput import qualified Data.Array as A import Data.Foldable+import Data.List (isSubsequenceOf, subsequences) import Data.Semigroup (Arg(..)) import Text.PrettyPrint @@ -25,14 +26,7 @@ main :: IO ()-main = defaultMain [ testGroup "sub props" [- slTest "empty in subs" prop_emptyInSubs,- slTest "self in subs" prop_selfInSubs,- slTest "count subs" prop_countSubs,- slTest "every sub is a sub" prop_everySubIsSub,- slTest2 "sub prop" prop_sub- ],- testGroup "diff props" [+main = defaultMain [ testGroup "diff props" [ slTest "lcsEmpty" prop_lcsEmpty, slTest "lcsSelf" prop_lcsSelf, slTest2 "lcsBoth" prop_lcsBoth,@@ -76,33 +70,7 @@ slTest s t = testProperty s $ forAll shortLists (t :: [Bool] -> Bool) slTest2 s t = testProperty s $ forAll2 shortLists (t :: [Bool] -> [Bool] -> Bool) --- We need some quick and dirty subsequence stuff for the diff tests,--- so we build that and some tests for it.---- | Determines whether one list is a subsequence of another.-isSub :: (Eq a) => [a] -> [a] -> Bool-isSub [] _ = True-isSub (_:_) [] = False-isSub (x:xs) (y:ys) | x == y = isSub xs ys- | otherwise = isSub (x:xs) ys---- | Lists the subsequences of a list.-subs :: [a] -> [[a]]-subs [] = [[]]-subs (x:rest) = map (x:) restss ++ restss- where restss = subs rest--prop_emptyInSubs = elem [] . subs-prop_selfInSubs xs = elem xs (subs xs)-prop_countSubs xs = length (subs xs) == 2^(length xs)-prop_sub xs ys = isSub xs ys == elem xs (subs ys)-prop_everySubIsSub xs = all (flip isSub xs) (subs xs)----- | Obtains a longest common subsequence of two lists using their--- diff. Note that there is an @lcs@ function in the--- 'Data.Algorithm.Diff' module, but it's not exported. It's trivial--- to reconstruct the LCS though, just by taking the 'B' elements.+-- | Obtains a longest common subsequence of two lists using their diff. diffLCS :: (Eq a) => [a] -> [a] -> [a] diffLCS xs ys = recoverLCS $ getDiff xs ys @@ -129,7 +97,12 @@ -- | Indicates whether a list is a longest common subsequence of two -- lists. isLCS :: (Eq a) => [a] -> [a] -> [a] -> Bool-isLCS ss xs ys = isSub ss ys && isSub ss ys && length ss == lenLCS xs ys+isLCS ss xs ys =+ and+ [ ss `isSubsequenceOf` xs,+ ss `isSubsequenceOf` ys,+ length ss == lenLCS xs ys+ ] -- | Computes the length of the longest common subsequence of two -- lists. This is a naive and inefficient recursive implementation@@ -167,8 +140,11 @@ let haskDiff=ppDiff $ getGroupedDiff le ri utilDiff= unsafePerformIO (runDiff (unlines le) (unlines ri)) in cover 90 (haskDiff == utilDiff) "exact match" $- classify (haskDiff == utilDiff) "exact match"- (div ((length (lines haskDiff))*100) (length (lines utilDiff)) < 110) -- less than 10% bigger+ classify (haskDiff == utilDiff) "exact match" $+ div+ (length (lines haskDiff)*100)+ (max 1 $ length $ lines utilDiff)+ < 110 -- less than 10% bigger where runDiff left right = do leftFile <- writeTemp left