diff --git a/Diff-liquidhaskell/Diff-liquidhaskell.cabal b/Diff-liquidhaskell/Diff-liquidhaskell.cabal index a1cca35..06eaeca 100644 --- a/Diff-liquidhaskell/Diff-liquidhaskell.cabal +++ b/Diff-liquidhaskell/Diff-liquidhaskell.cabal @@ -22,6 +22,7 @@ library Data.Algorithm.Diff Data.Algorithm.DiffOutput Data.Algorithm.DiffContext + Internal.LiftedFunctions build-depends: base >= 4.22.0.0 && < 5 , array diff --git a/Diff.cabal b/Diff.cabal index 8dad63a..0af8a74 100644 --- a/Diff.cabal +++ b/Diff.cabal @@ -42,6 +42,7 @@ library Data.Algorithm.Diff Data.Algorithm.DiffOutput Data.Algorithm.DiffContext + other-modules: Internal.LiftedFunctions ghc-options: -Wall -funbox-strict-fields source-repository head diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs index 576c04b..f231379 100644 --- a/src/Data/Algorithm/Diff.hs +++ b/src/Data/Algorithm/Diff.hs @@ -67,11 +67,17 @@ module Data.Algorithm.Diff -- * Finding chunks of differences , getGroupedDiff , getGroupedDiffBy + + -- * Predicates for LiquidHaskell specifications + , noStuttering + , noFFSS + , headIsFirst, headIsSecond, headIsBoth ) where import Prelude hiding (pi) import Data.Array (listArray, (!)) import Data.Bifunctor +import Internal.LiftedFunctions -- | /Diff Instruction/ — an internal enum recording the direction of a single -- non-diagonal edge traversed in the Myers edit graph. Every non-diagonal @@ -104,6 +110,7 @@ data DI = F | S deriving (Show, Eq) -- * '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) @@ -120,6 +127,64 @@ instance Bifunctor PolyDiff where -- | This is 'PolyDiff' specialized so both sides are the same type. type Diff a = PolyDiff a a +-- 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 }@-} + +{-@ type GroupedDiff a b = { d : ValidListDiff a b | nonEmptyDiff d } @-} + +{-@ +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 @-} +nonEmptyDiff :: PolyDiff [a] [b] -> Bool +nonEmptyDiff (First []) = False +nonEmptyDiff (Second []) = False +nonEmptyDiff (Both [] _) = False +nonEmptyDiff (Both _ []) = False +nonEmptyDiff _ = True + +{-@ 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 + -- | /D-path Location/ — a node on the wave front of the Myers O(ND) diff -- algorithm. -- @@ -333,6 +398,8 @@ getDiff = getDiffBy (==) -- -- > > 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 (==) @@ -352,20 +419,56 @@ getDiffBy eq a b = markup a b . reverse $ ses eq a b -- -- 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 [] = [] - - goFirsts (First x : xs) = let (fs, rest) = goFirsts xs in (x:fs, rest) - goFirsts xs = ([],xs) - - goSeconds (Second x : xs) = let (fs, rest) = goSeconds xs in (x:fs, rest) - goSeconds xs = ([],xs) - - goBoth (Both x y : xs) = let (fs, rest) = goBoth xs in ((x,y):fs, rest) - goBoth xs = ([],xs) +getGroupedDiffBy eq a b = groupDiff $ getDiffBy eq a b + +{-@ 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 [] = [] + +{-@ 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) + +{-@ 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) + +{-@ 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) diff --git a/src/Data/Algorithm/DiffContext.hs b/src/Data/Algorithm/DiffContext.hs index ea39035..18806da 100644 --- a/src/Data/Algorithm/DiffContext.hs +++ b/src/Data/Algorithm/DiffContext.hs @@ -1,3 +1,5 @@ +{-@ LIQUID "--ple" @-} +{-@ LIQUID "--ple-with-undecided-guards" @-} ----------------------------------------------------------------------------- -- | -- Module : Data.Algorithm.DiffContext @@ -20,13 +22,17 @@ module Data.Algorithm.DiffContext , unNumberContextDiff ) where -import Data.Algorithm.Diff (PolyDiff(..), Diff, getGroupedDiff) +import Data.Algorithm.Diff (PolyDiff(..), Diff, getGroupedDiff, + 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 = { h : [ValidListDiff c c] | noStuttering h} @-} -- | A 'Hunk' is a list of adjacent 'Diff's. -- -- No two consecutive elements in a 'Hunk' are both applications @@ -35,14 +41,40 @@ type ContextDiff c = [Hunk c] 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 :: Hunk c -> xs : [Diff [c]] -> [Hunk c] / [len xs] @-} + {-@ 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 @@ -73,9 +105,17 @@ unnumber (Numbered _ a) = a -- > i -- > j -- > -k +{-@ +getContextDiff :: + Eq a + => Maybe ContextSize + -> [a] + -> [a] + -> ContextDiff (Numbered a) +@-} getContextDiff :: Eq a - => Maybe Int -- ^ Context size. 'Nothing' means returning a whole-diff 'Hunk'. + => Maybe ContextSize -- ^ Context size. 'Nothing' means returning a whole-diff 'Hunk'. -> [a] -> [a] -> ContextDiff (Numbered a) @@ -84,6 +124,7 @@ getContextDiff contextSize a b = -- | If for some reason you need the line numbers stripped from the -- 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))) @@ -94,9 +135,17 @@ unNumberContextDiff = fmap (fmap (bimap (fmap unnumber) (fmap unnumber))) -- 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 ContextSize + -> [Numbered a] + -> [Numbered a] + -> ContextDiff (Numbered a) +@-} getContextDiffNumbered :: Eq a - => Maybe Int -- ^ Context size. 'Nothing' means returning a whole-diff 'Hunk'. + => Maybe ContextSize -- ^ Context size. 'Nothing' means returning a whole-diff 'Hunk'. -> [Numbered a] -> [Numbered a] -> ContextDiff (Numbered a) @@ -119,8 +168,11 @@ getContextDiffNumbered (Just contextSize) a0 b0 = -- 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 -> [Diff [c]] / [len h, 0]@-} - doPrefix :: Hunk c -> [Diff [c]] + {-@ doPrefix :: h : Hunk c + -> {v : [ValidListDiff c c] | noFFSS v + && (headIsFirst h <=> headIsFirst v) + && (headIsSecond h <=> headIsSecond v)} / [len h, 0] @-} + doPrefix :: [Diff [c]] -> [Diff [c]] doPrefix [] = [] -- Trailing common elements are no prefix. -- This case corresponds to when both input lists are identical, so the @@ -137,8 +189,11 @@ getContextDiffNumbered (Just contextSize) a0 b0 = -- -- Precondition: The input does not start with a 'Both' diff. Otherwise, -- it behaves like @doPrefix@. - {-@ doSuffix :: h : Hunk c -> [Diff [c]] / [len h, 1] @-} - doSuffix :: Hunk c -> [Diff [c]] + {-@ doSuffix :: h : Hunk c + -> {v : [ValidListDiff c c] | noFFSS v + && (headIsFirst h <=> headIsFirst v) + && (headIsSecond h <=> headIsSecond v)} / [len h, 1] @-} + doSuffix :: [Diff [c]] -> [Diff [c]] doSuffix [] = [] -- A trailing suffix. doSuffix [Both xs ys] = [Both (take contextSize xs) (take contextSize ys)] diff --git a/src/Internal/LiftedFunctions.hs b/src/Internal/LiftedFunctions.hs new file mode 100644 index 0000000..958a489 --- /dev/null +++ b/src/Internal/LiftedFunctions.hs @@ -0,0 +1,25 @@ +-- | Utilify functions lifted into Liquid Haskell logic. +-- +-- The /raison d'être/ for this module is that functions need to be explicitly +-- /lifted/ into the LiquidHaskell logic before we can call them in refinement +-- predicates. +-- In general, we need access to a functions unfoldings for the relevant constraints +-- to be produced. At the time of writing, GHC does not reliable exposes dependency +-- unfoldings in interface files; so the most robust work around is +-- to reimplement certain functions locally. +-- For a detailed discussion see: +-- +module Internal.LiftedFunctions where + +-- | 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