Interval.idr

module Interval

import Data.So

-- [TODO] Can we use a "parameters" block to avoid writing `Ord t =>` everywhere?

public export
rangeValid : Ord t => (closed : Bool) -> (lower: t) -> (upper: t) -> Bool
rangeValid closed lower upper = (ifThenElse closed (<=) (<)) lower upper

public export
data RangeInterval : (t : Type) -> {auto isOrd : Ord t} -> Type where
  Empty : Ord t => RangeInterval t
  Interval :
    Ord t =>
    (lower : t) ->
    (lowerClosed : Bool) ->
    (upper : t) ->
    (upperClosed : Bool) ->
    {auto 0 prfValid:
      let closed = lowerClosed && upperClosed in
      So (rangeValid closed lower upper)
    } ->
    RangeInterval t

public export
implementation Ord t => Show t => Show (RangeInterval t) where
  show Empty = "{∅}"
  show (Interval lo loCl hi hiCl) = concat [
    ifThenElse loCl "[" "(", show lo, ", ", show hi, ifThenElse hiCl "]" ")"
  ]

public export
implementation Ord t => Show t => Interpolation (RangeInterval t) where
  interpolate = show

isEmpty : Ord t => RangeInterval t -> Bool
isEmpty Empty = True
isEmpty _ = False

nonEmpty : Ord t => RangeInterval t -> Bool
nonEmpty Empty = False
nonEmpty _ = True

lowerMaybe : Ord t => RangeInterval t -> Maybe t
lowerMaybe Empty = Nothing
lowerMaybe (Interval lo _ _ _) = Just lo

upperMaybe : Ord t => RangeInterval t -> Maybe t
upperMaybe Empty = Nothing
upperMaybe (Interval _ _ hi _) = Just hi

public export
intersects : Ord t => (x : RangeInterval t) -> (y : RangeInterval t) -> Bool
intersects Empty _ = False
intersects _ Empty = False
-- [TODO] Check the math here
intersects (Interval x1 True x2 True) (Interval y1 True y2 True) = (x2 >= y1) || (y2 >= x1)
intersects (Interval x1 _    x2 _   ) (Interval y1 _    y2 _   ) = (x2 >  y1) || (y2 >  x1)


main : IO ()
main = let printShow = putStrLn . show in
  do
    printShow $ Empty
    printShow $ Interval 3 False 5 False
    printShow $ Interval 3 True 5 False
    printShow $ Interval 3 False 5 True
    printShow $ Interval 3 True 5 True
    -- Not allowed:
    -- printShow $ Interval 5 True 3 True