diff --git a/Diff-liquidhaskell/Diff-liquidhaskell.cabal b/Diff-liquidhaskell/Diff-liquidhaskell.cabal new file mode 100644 --- /dev/null +++ b/Diff-liquidhaskell/Diff-liquidhaskell.cabal @@ -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.. + -- 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 --git a/Diff.cabal b/Diff.cabal --- a/Diff.cabal +++ b/Diff.cabal @@ -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 -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 diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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/). diff --git a/bench/bench.hs b/bench/bench.hs new file mode 100644 --- /dev/null +++ b/bench/bench.hs @@ -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 + ] + ] diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs --- a/src/Data/Algorithm/Diff.hs +++ b/src/Data/Algorithm/Diff.hs @@ -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)/ --- . +-- [/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 Bool>. + i : Nat -> j : Nat -> xs : [DL] + -> { m : Maybe {dl : DL | 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 diff --git a/src/Data/Algorithm/Diff/Refinement.hs b/src/Data/Algorithm/Diff/Refinement.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algorithm/Diff/Refinement.hs @@ -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 diff --git a/src/Data/Algorithm/Diff/Type.hs b/src/Data/Algorithm/Diff/Type.hs new file mode 100644 --- /dev/null +++ b/src/Data/Algorithm/Diff/Type.hs @@ -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 diff --git a/src/Data/Algorithm/DiffContext.hs b/src/Data/Algorithm/DiffContext.hs --- a/src/Data/Algorithm/DiffContext.hs +++ b/src/Data/Algorithm/DiffContext.hs @@ -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. diff --git a/src/Data/Algorithm/DiffOutput.hs b/src/Data/Algorithm/DiffOutput.hs --- a/src/Data/Algorithm/DiffOutput.hs +++ b/src/Data/Algorithm/DiffOutput.hs @@ -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) diff --git a/test/Test.hs b/test/Test.hs --- a/test/Test.hs +++ b/test/Test.hs @@ -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