Add Hunk invariant static checks

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.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

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)

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)]

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:
+-- <https://www.tweag.io/blog/2024-09-12-lh-reflection/>
+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