Intervals.hs

{-@ LIQUID "--no-termination" @-}

module Intervals where

type Offset = Int

-- | Invariant: Intervals are non-empty
{-@ data Interval = I
      { from :: Int
      , to   :: {v: Int | from < v }
      }
  @-}
data Interval  = I { from :: Offset, to :: Offset }

-- | Invariant: Intervals are sorted, disjoint and non-adjacent
{-@ type OrdIntervals N = [{v:Interval | N <= from v}]<{\fld v -> (to fld <= from v)}> @-}
type OrdIntervals = [Interval]

-- | Invariant: Intervals start with lower-bound of 0
{-@ data Intervals = Intervals { itvs :: OrdIntervals 0 } @-}
data Intervals = Intervals {itvs :: OrdIntervals }

-- | Invariant as a Haskell Predicate
{-@ okIntervals :: lb:Nat -> is:OrdIntervals lb -> {v : Bool | v } / [len is] @-}
okIntervals :: Int -> OrdIntervals -> Bool
okIntervals _ []            = True
okIntervals lb ((I f t) : is) = lb <= f && f < t && okIntervals t is

--------------------------------------------------------------------------------
-- | Unit tests
--------------------------------------------------------------------------------
okItv  = I 10 20
badItv = I 20 10

okItvs  = Intervals [I 10 20, I 30 40, I 40 50]
badItvs = Intervals [I 10 20, I 40 50, I 30 40]

--------------------------------------------------------------------------------
-- | Intersection
--------------------------------------------------------------------------------
intersect :: Intervals -> Intervals -> Intervals
intersect (Intervals is1) (Intervals is2) = Intervals (go 0 is1 is2)
  where
    {- AUTO! go :: lb:Int -> is1:OrdIntervals lb -> is2:OrdIntervals lb -> OrdIntervals lb @-}
    go :: Int -> OrdIntervals -> OrdIntervals -> OrdIntervals
    go _ _ [] = []
    go _ [] _ = []
    go lb (i1@(I f1 t1) : is1) (i2@(I f2 t2) : is2)
      -- reorder for symmetry
      | t1 < t2   = go lb (i2:is2) (i1:is1)
      -- disjoint
      | f1 >= f2  = go lb (i1:is1) is2
      -- subset
      | t1 == t2  = I f' t2 : go t2 is1 is2
      -- overlapping
      | otherwise = I f' t2 : go t2 ((I t2 t1) : is1) is2
      where
        f'        = max f1 f2

--------------------------------------------------------------------------------
-- | Union
--------------------------------------------------------------------------------
union :: Intervals -> Intervals -> Intervals
union (Intervals is1) (Intervals is2) = Intervals (go 0 is1 is2)
  where
    {- AUTO! go :: lb:Int -> is1:OrdIntervals lb -> is2:OrdIntervals lb -> OrdIntervals lb @-}
    go _ is [] = is
    go _ [] is = is
    go lb (i1@(I f1 t1) : is1) (i2@(I f2 t2) : is2)
      -- reorder for symmetry
      | t1 < t2 = go lb (i2:is2) (i1:is1)
      -- disjoint
      | f1 > t2 = i2 : go t2 (i1:is1) is2
      -- overlapping
      | otherwise  = go lb (i1 { from = f'} : is1) is2
      where f' = min (from i1) (from i2)

--------------------------------------------------------------------------------
-- | Difference
--------------------------------------------------------------------------------
subtract :: Intervals -> Intervals -> Intervals
subtract (Intervals is1) (Intervals is2) = Intervals (go 0 is1 is2)
  where
    {- AUTO! go :: lb:Int -> is1:OrdIntervals lb -> is2:OrdIntervals lb -> OrdIntervals lb @-}
    go _ is [] = is
    go _ [] _  = []
    go lb (i1@(I f1 t1) : is1) (i2@(I f2 t2) : is2)
      -- i2 past i1
      | t1 <= f2 = i1 : go t1 is1 (i2:is2)
      -- i1 past i2
      | t2 <= f1 = go lb (i1:is1) is2
      -- i1 contained in i2
      | f2 <= f1 , t1 <= t2 = go lb is1 (i2:is2)
      -- i2 covers beginning of i1
      | f1 >= f2 = go t2 (i1 { from = t2} : is1) is2
      -- i2 covers end of i1
      | t1 <= t2 = i1 { to = f2 } : go f2 is1 (i2:is2)
      -- i2 in the middle of i1
      | otherwise = I f1 f2 : go f2 (I t2 t1 : is1) is2