-- | 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 :: forall a b. PolyDiff [a] [b] -> Bool
validListDiff (Both [a]
xs [b]
ys) = [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
ys
validListDiff (First [a]
_) = Bool
True
validListDiff (Second [b]
_) = Bool
True

{-@ inline nonEmptyDiff @-}
-- | True when the diff is not empty on either side.
nonEmptyDiff :: PolyDiff [a] [b] -> Bool
nonEmptyDiff :: forall a b. PolyDiff [a] [b] -> Bool
nonEmptyDiff (First []) = Bool
False
nonEmptyDiff (Second []) = Bool
False
nonEmptyDiff (Both [] [b]
_) = Bool
False
nonEmptyDiff (Both [a]
_ []) = Bool
False
nonEmptyDiff PolyDiff [a] [b]
_ = Bool
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 :: forall a b. [PolyDiff a b] -> Bool
headIsFirst (First a
_ : [PolyDiff a b]
_) = Bool
True
headIsFirst [PolyDiff a b]
_ = Bool
False
headIsSecond :: forall a b. [PolyDiff a b] -> Bool
headIsSecond (Second b
_ : [PolyDiff a b]
_) = Bool
True
headIsSecond [PolyDiff a b]
_ = Bool
False
headIsBoth :: forall a b. [PolyDiff a b] -> Bool
headIsBoth (Both a
_ b
_ : [PolyDiff a b]
_) = Bool
True
headIsBoth [PolyDiff a b]
_ = Bool
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 :: forall a b. [PolyDiff a b] -> Bool
noStuttering [] = Bool
True
noStuttering (First a
_ : [PolyDiff a b]
xs) = Bool -> Bool
not ([PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
headIsFirst [PolyDiff a b]
xs) Bool -> Bool -> Bool
&& [PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
noStuttering [PolyDiff a b]
xs
noStuttering (Second b
_ : [PolyDiff a b]
xs) = Bool -> Bool
not ([PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
headIsSecond [PolyDiff a b]
xs) Bool -> Bool -> Bool
&& [PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
noStuttering [PolyDiff a b]
xs
noStuttering (Both a
_ b
_ : [PolyDiff a b]
xs) = Bool -> Bool
not ([PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
headIsBoth [PolyDiff a b]
xs) Bool -> Bool -> Bool
&& [PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
noStuttering [PolyDiff a b]
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 :: forall a b. [PolyDiff a b] -> Bool
noFFSS [] = Bool
True
noFFSS (First a
_ : [PolyDiff a b]
xs) = Bool -> Bool
not ([PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
headIsFirst [PolyDiff a b]
xs) Bool -> Bool -> Bool
&& [PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
noFFSS [PolyDiff a b]
xs
noFFSS (Second b
_ : [PolyDiff a b]
xs) = Bool -> Bool
not ([PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
headIsSecond [PolyDiff a b]
xs) Bool -> Bool -> Bool
&& [PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
noFFSS [PolyDiff a b]
xs
noFFSS (Both a
_ b
_ : [PolyDiff a b]
xs) = [PolyDiff a b] -> Bool
forall a b. [PolyDiff a b] -> Bool
noFFSS [PolyDiff a b]
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 :: forall a b c. (a, b, c) -> a
fst3 (a
x, b
_, c
_) = a
x
snd3 :: (a, b, c) -> b
snd3 :: forall a b c. (a, b, c) -> b
snd3 (a
_, b
y, c
_) = b
y
thd3 :: (a, b, c) -> c
thd3 :: forall a b c. (a, b, c) -> c
thd3 (a
_, b
_, c
z) = c
z