{-@ 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
-- Copyright   :  (c) Sterling Clover 2008-2011, Kevin Charter 2011
-- License     :  BSD 3 Clause
-- Maintainer  :  s.clover@gmail.com
-- Stability   :  experimental
-- Portability :  portable
--
-- This is an implementation of the diff algorithm as described in
-- [/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
    , getDiff
    , getDiffBy

    -- * Finding chunks of differences
    , getGroupedDiff
    , getGroupedDiffBy
    ) where

import Prelude hiding (pi)
import Data.Array (listArray, (!))
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 (Int -> DI -> ShowS
[DI] -> ShowS
DI -> String
(Int -> DI -> ShowS)
-> (DI -> String) -> ([DI] -> ShowS) -> Show DI
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DI -> ShowS
showsPrec :: Int -> DI -> ShowS
$cshow :: DI -> String
show :: DI -> String
$cshowList :: [DI] -> ShowS
showList :: [DI] -> ShowS
Show, DI -> DI -> Bool
(DI -> DI -> Bool) -> (DI -> DI -> Bool) -> Eq DI
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DI -> DI -> Bool
== :: DI -> DI -> Bool
$c/= :: DI -> DI -> Bool
/= :: DI -> DI -> Bool
Eq)

-- | /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
    { DL -> Int
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.
    , DL -> Int
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.
    , DL -> [DI]
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 (Int -> DL -> ShowS
[DL] -> ShowS
DL -> String
(Int -> DL -> ShowS)
-> (DL -> String) -> ([DL] -> ShowS) -> Show DL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DL -> ShowS
showsPrec :: Int -> DL -> ShowS
$cshow :: DL -> String
show :: DL -> String
$cshowList :: [DL] -> ShowS
showList :: [DL] -> ShowS
Show, DL -> DL -> Bool
(DL -> DL -> Bool) -> (DL -> DL -> Bool) -> Eq DL
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DL -> DL -> Bool
== :: DL -> DL -> Bool
$c/= :: DL -> DL -> Bool
/= :: DL -> DL -> Bool
Eq)

{-@ 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 :: DL -> DL -> DL
furthestReaching DL
x DL
y
  | DL -> Int
poi DL
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= DL -> Int
poi DL
y = DL
x
  | Bool
otherwise      = DL
y

-- | 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 :: forall a b.
(a -> b -> Bool) -> [a] -> [b] -> Int -> Int -> Int -> Int -> Bool
canDiag a -> b -> Bool
eq [a]
as [b]
bs Int
lena Int
lenb = \Int
i Int
j ->
  (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
lena Bool -> Bool -> Bool
&& Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
lenb) Bool -> Bool -> Bool
&& ((Array Int a
arAs Array Int a -> Int -> a
forall i e. Ix i => Array i e -> i -> e
! Int
i) a -> b -> Bool
`eq` (Array Int b
arBs Array Int b -> Int -> b
forall i e. Ix i => Array i e -> i -> e
! Int
j))
  where
    -- Lists are converted into arrays to have O(1) lookups.
    arAs :: Array Int a
arAs = (Int, Int) -> [a] -> Array Int a
forall i e. Ix i => (i, i) -> [e] -> Array i e
listArray (Int
0,Int
lena Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [a]
as
    arBs :: Array Int b
arBs = (Int, Int) -> [b] -> Array Int b
forall i e. Ix i => (i, i) -> [e] -> Array i e
listArray (Int
0,Int
lenb Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [b]
bs

{-@ reflect hStep @-}
hStep :: DL -> DL
hStep :: DL -> DL
hStep DL
node = DL
node {poi = poi node + 1, path = F : path node}

{-@ reflect vStep @-}
vStep :: DL -> DL
vStep :: DL -> DL
vStep DL
node = DL
node {poj = poj node + 1, path = S : path node}

-- | 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 :: Int -> Int -> (Int -> Int -> Bool) -> Int -> [DL] -> [DL]
dstep Int
lena Int
lenb Int -> Int -> Bool
_ Int
_d [] = String -> [DL]
forall a. HasCallStack => String -> a
error String
"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 Int
lena Int
lenb Int -> Int -> Bool
cd Int
_ (DL
dl:[DL]
dls) =
  if DL -> Int
poi DL
dl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lena then DL -> [DL] -> [DL]
stepAndMerge DL
dl [DL]
dls
  else
    (Int -> Int -> (Int -> Int -> Bool) -> DL -> DL
addsnake Int
lena Int
lenb Int -> Int -> Bool
cd (DL -> DL
hStep DL
dl) DL -> [DL] -> [DL]
forall a. a -> [a] -> [a]
: DL -> [DL] -> [DL]
stepAndMerge DL
dl [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.
      [DL] -> () -> [DL]
forall a b. a -> b -> a
`const` Int -> Int -> DL -> [DL] -> ()
_wfDistanceLowerBound Int
lena Int
lenb DL
dl [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 :: DL -> [DL] -> [DL]
stepAndMerge DL
prev [DL]
nodes =
      -- When a node lies in the bottom boundary no subsequent node can reach
      -- the goal faster. See lemma '_wfDistanceLowerBound'.
      if DL -> Int
poj DL
prev Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lenb then []
      else case [DL]
nodes of
        [] -> [Int -> Int -> (Int -> Int -> Bool) -> DL -> DL
addsnake Int
lena Int
lenb Int -> Int -> Bool
cd (DL -> DL) -> DL -> DL
forall a b. (a -> b) -> a -> b
$ DL -> DL
vStep DL
prev]
        (DL
next:[DL]
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 DL -> Int
poi DL
next Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lena then DL -> DL
vStep DL
prev DL -> [DL] -> [DL]
forall a. a -> [a] -> [a]
: DL -> [DL] -> [DL]
stepAndMerge DL
next [DL]
rest
            else
              (Int -> Int -> (Int -> Int -> Bool) -> DL -> DL
addsnake Int
lena Int
lenb Int -> Int -> Bool
cd (DL -> DL -> DL
furthestReaching (DL -> DL
vStep DL
prev) (DL -> DL
hStep DL
next)) DL -> [DL] -> [DL]
forall a. a -> [a] -> [a]
: DL -> [DL] -> [DL]
stepAndMerge DL
next [DL]
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.
                [DL] -> () -> [DL]
forall a b. a -> b -> a
`const` Int -> Int -> DL -> [DL] -> ()
_wfDistanceLowerBound Int
lena Int
lenb DL
next [DL]
rest

-- | 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 :: Int -> Int -> (Int -> Int -> Bool) -> DL -> DL
addsnake Int
lena Int
lenb Int -> Int -> Bool
cd DL
dl
    | Int -> Int -> Bool
cd Int
pi Int
pj = Int -> Int -> (Int -> Int -> Bool) -> DL -> DL
addsnake Int
lena Int
lenb Int -> Int -> Bool
cd (DL -> DL) -> DL -> DL
forall a b. (a -> b) -> a -> b
$
                 DL
dl {poi = pi + 1, poj = pj + 1, path = path dl}
    | Bool
otherwise   = DL
dl
    where pi :: Int
pi = DL -> Int
poi DL
dl; pj :: Int
pj = DL -> Int
poj DL
dl

-- | 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 :: forall a b. (a -> b -> Bool) -> [a] -> [b] -> [DI]
ses a -> b -> Bool
eq [a]
as [b]
bs = DL -> [DI]
path (DL -> [DI]) -> DL -> [DI]
forall a b. (a -> b) -> a -> b
$ Int -> [DL] -> DL
searchEndpoint Int
0 [Int -> Int -> (Int -> Int -> Bool) -> DL -> DL
addsnake Int
lena Int
lenb Int -> Int -> Bool
cd (Int -> Int -> [DI] -> DL
DL Int
0 Int
0 [])]
  where
    cd :: Int -> Int -> Bool
cd = (a -> b -> Bool) -> [a] -> [b] -> Int -> Int -> Int -> Int -> Bool
forall a b.
(a -> b -> Bool) -> [a] -> [b] -> Int -> Int -> Int -> Int -> Bool
canDiag a -> b -> Bool
eq [a]
as [b]
bs Int
lena Int
lenb
    lena :: Int
lena = [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
as; lenb :: Int
lenb = [b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
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 :: Int -> [DL] -> DL
searchEndpoint Int
_ [] = String -> DL
forall a. HasCallStack => String -> a
error String
"ses: The search must have a seed node"
    searchEndpoint Int
d [DL]
wf = case Int -> Int -> [DL] -> Maybe DL
findEndpoint Int
lena Int
lenb [DL]
wf of
      Just DL
p  -> DL
p
      Maybe DL
Nothing -> let wf' :: [DL]
wf' = Int -> Int -> (Int -> Int -> Bool) -> Int -> [DL] -> [DL]
dstep Int
lena Int
lenb Int -> Int -> Bool
cd Int
d [DL]
wf
                     _lemmaNonNeg :: ()
_lemmaNonNeg = Int -> Int -> [DL] -> ()
_minDistanceNonNegative Int
lena Int
lenb [DL]
wf'
                  in Int -> [DL] -> DL
searchEndpoint (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [DL]
wf'
    -- The abstract refinement @q@ lets 'find' carry the wave
    -- front element refinement (notably @len (path dl) == d@)
    -- over to the returned endpoint.
    {-@ assume findEndpoint
          :: forall <q :: DL -> Bool>.
             i : Nat -> j : Nat -> xs : [DL<q>]
          -> { m : Maybe {dl : DL<q> | endPoint i j dl}
             | m == Nothing => _wfDistanceToGoal i j xs > 0} @-}
    findEndpoint :: Int -> Int -> [DL] -> Maybe DL
    findEndpoint :: Int -> Int -> [DL] -> Maybe DL
findEndpoint Int
i Int
j = (DL -> Bool) -> [DL] -> Maybe DL
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Int -> Int -> DL -> Bool
endPoint Int
i Int
j)

-- | Takes two lists and returns a list of differences between them. This is
-- 'getDiffBy' with '==' used as predicate.
--
-- > > getDiff ["a","b","c","d","e"] ["a","c","d","f"]
-- > [Both "a" "a",First "b",Both "c" "c",Both "d" "d",First "e",Second "f"]
-- > > getDiff "abcde" "acdf"
-- > [Both 'a' 'a',First 'b',Both 'c' 'c',Both 'd' 'd',First 'e',Second 'f']
getDiff :: (Eq a) => [a] -> [a] -> [Diff a]
getDiff :: forall a. Eq a => [a] -> [a] -> [Diff a]
getDiff = (a -> a -> Bool) -> [a] -> [a] -> [PolyDiff a a]
forall a b. (a -> b -> Bool) -> [a] -> [b] -> [PolyDiff a b]
getDiffBy a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

-- | Takes two lists and returns a list of differences between them, grouped
-- into chunks. This is 'getGroupedDiffBy' with '==' used as predicate.
--
-- > > 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 :: forall a. Eq a => [a] -> [a] -> [Diff [a]]
getGroupedDiff = (a -> a -> Bool) -> [a] -> [a] -> [PolyDiff [a] [a]]
forall a b. (a -> b -> Bool) -> [a] -> [b] -> [PolyDiff [a] [b]]
getGroupedDiffBy a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

-- | 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 :: forall a b. (a -> b -> Bool) -> [a] -> [b] -> [PolyDiff a b]
getDiffBy a -> b -> Bool
eq [a]
a [b]
b = [a] -> [b] -> [DI] -> [PolyDiff a b]
markup [a]
a [b]
b ([DI] -> [PolyDiff a b])
-> ([DI] -> [DI]) -> [DI] -> [PolyDiff a b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DI] -> [DI]
forall a. [a] -> [a]
reverse ([DI] -> [PolyDiff a b]) -> [DI] -> [PolyDiff a b]
forall a b. (a -> b) -> a -> b
$ (a -> b -> Bool) -> [a] -> [b] -> [DI]
forall a b. (a -> b -> Bool) -> [a] -> [b] -> [DI]
ses a -> b -> Bool
eq [a]
a [b]
b
    where markup :: [a] -> [b] -> [DI] -> [PolyDiff a b]
markup (a
x:[a]
xs) (b
y:[b]
ys) [DI]
ds
            | a -> b -> Bool
eq a
x b
y = a -> b -> PolyDiff a b
forall a b. a -> b -> PolyDiff a b
Both a
x b
y PolyDiff a b -> [PolyDiff a b] -> [PolyDiff a b]
forall a. a -> [a] -> [a]
: [a] -> [b] -> [DI] -> [PolyDiff a b]
markup [a]
xs [b]
ys [DI]
ds
          markup (a
x:[a]
xs)   [b]
ys   (DI
F:[DI]
ds) = a -> PolyDiff a b
forall a b. a -> PolyDiff a b
First a
x  PolyDiff a b -> [PolyDiff a b] -> [PolyDiff a b]
forall a. a -> [a] -> [a]
: [a] -> [b] -> [DI] -> [PolyDiff a b]
markup [a]
xs [b]
ys [DI]
ds
          markup   [a]
xs   (b
y:[b]
ys) (DI
S:[DI]
ds) = b -> PolyDiff a b
forall a b. b -> PolyDiff a b
Second b
y PolyDiff a b -> [PolyDiff a b] -> [PolyDiff a b]
forall a. a -> [a] -> [a]
: [a] -> [b] -> [DI] -> [PolyDiff a b]
markup [a]
xs [b]
ys [DI]
ds
          markup [a]
_ [b]
_ [DI]
_ = []

-- | 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 :: forall a b. (a -> b -> Bool) -> [a] -> [b] -> [PolyDiff [a] [b]]
getGroupedDiffBy a -> b -> Bool
eq [a]
a [b]
b = [PolyDiff a b] -> [PolyDiff [a] [b]]
forall a b. [PolyDiff a b] -> [PolyDiff [a] [b]]
groupDiff ([PolyDiff a b] -> [PolyDiff [a] [b]])
-> [PolyDiff a b] -> [PolyDiff [a] [b]]
forall a b. (a -> b) -> a -> b
$ (a -> b -> Bool) -> [a] -> [b] -> [PolyDiff a b]
forall a b. (a -> b -> Bool) -> [a] -> [b] -> [PolyDiff a b]
getDiffBy a -> b -> Bool
eq [a]
a [b]
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 :: forall a b. [PolyDiff a b] -> [PolyDiff [a] [b]]
groupDiff (First a
x  : [PolyDiff a b]
xs) = let ([a]
fs, [PolyDiff a b]
rest) = [PolyDiff a b] -> ([a], [PolyDiff a b])
forall a b. [PolyDiff a b] -> ([a], [PolyDiff a b])
leadingFirsts  [PolyDiff a b]
xs
                                 in [a] -> PolyDiff [a] [b]
forall a b. a -> PolyDiff a b
First (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
fs) PolyDiff [a] [b] -> [PolyDiff [a] [b]] -> [PolyDiff [a] [b]]
forall a. a -> [a] -> [a]
: [PolyDiff a b] -> [PolyDiff [a] [b]]
forall a b. [PolyDiff a b] -> [PolyDiff [a] [b]]
groupDiff [PolyDiff a b]
rest
    groupDiff (Second b
x : [PolyDiff a b]
xs) = let ([b]
sc, [PolyDiff a b]
rest) = [PolyDiff a b] -> ([b], [PolyDiff a b])
forall a b. [PolyDiff a b] -> ([b], [PolyDiff a b])
leadingSeconds [PolyDiff a b]
xs
                                 in [b] -> PolyDiff [a] [b]
forall a b. b -> PolyDiff a b
Second (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
sc) PolyDiff [a] [b] -> [PolyDiff [a] [b]] -> [PolyDiff [a] [b]]
forall a. a -> [a] -> [a]
: [PolyDiff a b] -> [PolyDiff [a] [b]]
forall a b. [PolyDiff a b] -> [PolyDiff [a] [b]]
groupDiff [PolyDiff a b]
rest
    groupDiff (Both a
x b
y : [PolyDiff a b]
xs) = let ([a]
bxs, [b]
bys, [PolyDiff a b]
rest) = [PolyDiff a b] -> ([a], [b], [PolyDiff a b])
forall a b. [PolyDiff a b] -> ([a], [b], [PolyDiff a b])
leadingBoths [PolyDiff a b]
xs
                                 in [a] -> [b] -> PolyDiff [a] [b]
forall a b. a -> b -> PolyDiff a b
Both (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
bxs) (b
yb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
bys) PolyDiff [a] [b] -> [PolyDiff [a] [b]] -> [PolyDiff [a] [b]]
forall a. a -> [a] -> [a]
: [PolyDiff a b] -> [PolyDiff [a] [b]]
forall a b. [PolyDiff a b] -> [PolyDiff [a] [b]]
groupDiff [PolyDiff a b]
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 :: forall a b. [PolyDiff a b] -> ([a], [PolyDiff a b])
leadingFirsts (First a
y : [PolyDiff a b]
diffs) = let ([a]
firsts, [PolyDiff a b]
rest) = [PolyDiff a b] -> ([a], [PolyDiff a b])
forall a b. [PolyDiff a b] -> ([a], [PolyDiff a b])
leadingFirsts [PolyDiff a b]
diffs
                                       in (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
firsts, [PolyDiff a b]
rest)
    leadingFirsts [PolyDiff a b]
diffs = ([],[PolyDiff a b]
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 :: forall a b. [PolyDiff a b] -> ([b], [PolyDiff a b])
leadingSeconds (Second b
y : [PolyDiff a b]
diffs) = let ([b]
seconds, [PolyDiff a b]
rest) = [PolyDiff a b] -> ([b], [PolyDiff a b])
forall a b. [PolyDiff a b] -> ([b], [PolyDiff a b])
leadingSeconds [PolyDiff a b]
diffs
                                         in (b
yb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
seconds, [PolyDiff a b]
rest)
    leadingSeconds [PolyDiff a b]
diffs = ([],[PolyDiff a b]
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 :: forall a b. [PolyDiff a b] -> ([a], [b], [PolyDiff a b])
leadingBoths (Both a
w b
z : [PolyDiff a b]
diffs) = let ([a]
as, [b]
bs, [PolyDiff a b]
rest) = [PolyDiff a b] -> ([a], [b], [PolyDiff a b])
forall a b. [PolyDiff a b] -> ([a], [b], [PolyDiff a b])
leadingBoths [PolyDiff a b]
diffs
                                       in (a
wa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
as, b
zb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
bs, [PolyDiff a b]
rest)
    leadingBoths [PolyDiff a b]
diffs = ([], [], [PolyDiff a b]
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 -> Int
_kdiag DL
dl = DL -> Int
poi DL
dl Int -> Int -> Int
forall a. Num a => a -> a -> a
- DL -> Int
poj DL
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 :: Int -> [DL] -> Bool
_wfDiags Int
_ [] = Bool
True
_wfDiags Int
k (DL
dl:[DL]
dls) = DL -> Int
_kdiag DL
dl Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k Bool -> Bool -> Bool
&& Int -> [DL] -> Bool
_wfDiags (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) [DL]
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 :: Int -> Int -> DL -> Int
_manhattanDistance Int
lena Int
lenb DL
dl  = Int
lena Int -> Int -> Int
forall a. Num a => a -> a -> a
- (DL -> Int
poi DL
dl) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
lenb Int -> Int -> Int
forall a. Num a => a -> a -> a
- (DL -> Int
poj DL
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 :: Int -> Int -> [DL] -> Int
_wfDistanceToGoal Int
lena Int
lenb [] = Int
lena Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
lenb Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2
_wfDistanceToGoal Int
lena Int
lenb (DL
dl:[DL]
dls) =
  -- We avoid using 'min' here so that LH can unfold this definition.
  if Int -> Int -> DL -> Int
_manhattanDistance Int
lena Int
lenb DL
dl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Int -> [DL] -> Int
_wfDistanceToGoal Int
lena Int
lenb [DL]
dls
  then Int -> Int -> DL -> Int
_manhattanDistance Int
lena Int
lenb DL
dl
  else Int -> Int -> [DL] -> Int
_wfDistanceToGoal Int
lena Int
lenb [DL]
dls

{-@ inline _reducesDistanceToGoal @-}
_reducesDistanceToGoal :: Int -> Int -> [DL] -> [DL] -> Bool
_reducesDistanceToGoal :: Int -> Int -> [DL] -> [DL] -> Bool
_reducesDistanceToGoal Int
lena Int
lenb [DL]
wf1 [DL]
wf2 =
  Int -> Int -> [DL] -> Int
_wfDistanceToGoal Int
lena Int
lenb [DL]
wf2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Int -> [DL] -> Int
_wfDistanceToGoal Int
lena Int
lenb [DL]
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 :: Int -> Int -> DL -> Bool
_withinBounds Int
lena Int
lenb DL
dl = DL -> Int
poi DL
dl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lena Bool -> Bool -> Bool
&& DL -> Int
poj DL
dl Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lenb

{-@ inline endPoint @-}
endPoint :: Int -> Int -> DL -> Bool
endPoint :: Int -> Int -> DL -> Bool
endPoint Int
lena Int
lenb DL
dl = DL -> Int
poi DL
dl Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
lena Bool -> Bool -> Bool
&& DL -> Int
poj DL
dl Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
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 :: Int -> Int -> Int -> [DL] -> ()
_wfDistanceLowerBoundK Int
_    Int
_    Int
_ []      = ()
_wfDistanceLowerBoundK Int
lena Int
lenb Int
k (DL
_:[DL]
dls) = Int -> Int -> Int -> [DL] -> ()
_wfDistanceLowerBoundK Int
lena Int
lenb (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) [DL]
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 :: Int -> Int -> DL -> [DL] -> ()
_wfDistanceLowerBound Int
lena Int
lenb DL
prev [] = ()
_wfDistanceLowerBound Int
lena Int
lenb DL
prev xs :: [DL]
xs@(DL
_:[DL]
_) = ()
  where
    _lemma :: ()
_lemma = Int -> Int -> Int -> [DL] -> ()
_wfDistanceLowerBoundK Int
lena Int
lenb (DL -> Int
_kdiag DL
prev Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) [DL]
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 :: Int -> Int -> [DL] -> ()
_minDistanceNonNegative Int
_    Int
_    []       = ()
_minDistanceNonNegative Int
lena Int
lenb (DL
_:[DL]
dls) = Int -> Int -> [DL] -> ()
_minDistanceNonNegative Int
lena Int
lenb [DL]
dls