{-# LANGUAGE NoImplicitPrelude
  #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Math.Combinatorics.Species.Util.Interval
-- Copyright   :  (c) Brent Yorgey 2010
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  byorgey@cis.upenn.edu
-- Stability   :  experimental
--
-- A simple implementation of intervals of natural numbers, for use in
-- tracking the possible sizes of structures of a species.  For
-- example, the species @x + x^2 + x^3@ will correspond to the
-- interval [1,3].
--
-----------------------------------------------------------------------------

module Math.Combinatorics.Species.Util.Interval
    (
    -- * The 'NatO' type
      NatO, omega, natO

    -- * The 'Interval' type
    , Interval, iLow, iHigh

    -- * Interval operations
    , decrI, union, intersect, elem, toList

    -- * Constructing intervals
    , natsI, fromI, emptyI, omegaI
    ) where

import NumericPrelude
import PreludeBase hiding (elem)

import qualified Algebra.Additive as Additive
import qualified Algebra.Ring as Ring

-- | 'NatO' is an explicit representation of the co-inductive Nat type
--   which admits an infinite value, omega.  Our intuition for the
--   semantics of 'NatO' comes from thinking of it as an efficient
--   representation of lazy unary natural numbers, except that we can
--   actually test for omega in finite time.
data NatO = Nat Integer | Omega
  deriving (Eq, Ord, Show)

-- | The infinite 'NatO' value.
omega :: NatO
omega = Omega

-- | Eliminator for 'NatO' values.
natO :: (Integer -> a) -> a -> NatO -> a
natO _ o Omega = o
natO f _ (Nat n) = f n

-- | Decrement a possibly infinite natural. TZero and omega are both
--   fixed points of 'decr'.
decr :: NatO -> NatO
decr (Nat 0) = Nat 0
decr (Nat n) = Nat (n-1)
decr Omega   = Omega

-- | 'NatO' forms an additive monoid, with zero as the identity.  This
--   doesn't quite fit since Additive.C is supposed to be for groups,
--   so the 'negate' method just throws an error.  But we'll never use
--   it and 'NatO' won't be directly exposed to users of the species
--   library anyway.
instance Additive.C NatO where
  zero          = Nat 0
  Nat m + Nat n = Nat (m + n)
  _ + _         = Omega
  negate = error "naturals with omega only form a semiring"

-- | In fact, 'NatO' forms a semiring, with 1 as the multiplicative
--   unit.
instance Ring.C NatO where
  one = Nat 1
  Nat 0 * _     = Nat 0
  _ * Nat 0     = Nat 0
  Nat m * Nat n = Nat (m * n)
  _ * _         = Omega

  fromInteger = Nat

-- | An 'Interval' is a closed range of consecutive integers.  Both
--   endpoints are represented as 'NatO' values.  For example, [2,5]
--   represents the values 2,3,4,5; [2,omega] represents all integers
--   greater than 1; intervals where the first endpoint is greater than the
--   second also represent the empty interval.
data Interval = I { iLow  :: NatO -- ^ Get the lower endpoint of an 'Interval'
                  , iHigh :: NatO -- ^ Get the upper endpoint of an 'Interval'
                  }
  deriving Show

-- | Decrement both endpoints of an interval.
decrI :: Interval -> Interval
decrI (I l h) = I (decr l) (decr h)

-- | The union of two intervals is the smallest interval containing
--   both.
union :: Interval -> Interval -> Interval
union (I l1 h1) (I l2 h2) = I (min l1 l2) (max h1 h2)

-- | The intersection of two intervals is the largest interval
--   contained in both.
intersect :: Interval -> Interval -> Interval
intersect (I l1 h1) (I l2 h2) = I (max l1 l2) (min h1 h2)

-- | Intervals can be added by adding their endpoints pointwise.
instance Additive.C Interval where
  zero = I 0 0
  (I l1 h1) + (I l2 h2) = I (l1 + l2) (h1 + h2)
  negate = error "Interval negation: intervals only form a semiring"

-- | Intervals form a semiring, with the multiplication operation
--   being pointwise multiplication of their endpoints.
instance Ring.C Interval where
  one = I 1 1
  (I l1 h1) * (I l2 h2) = I (l1 * l2) (h1 * h2)
  fromInteger n = I (Nat n) (Nat n)

-- | Test a given integer for interval membership.
elem :: Integer -> Interval -> Bool
elem n (I lo Omega)    = lo <= fromInteger n
elem n (I lo (Nat hi)) = lo <= fromInteger n && n <= hi

-- | Convert an interval to a list of Integers.
toList :: Interval -> [Integer]
toList (I Omega Omega) = []
toList (I lo hi) | lo > hi = []
toList (I (Nat lo) Omega) = [lo..]
toList (I (Nat lo) (Nat hi)) = [lo..hi]

-- | The range [0,omega] containing all natural numbers.
natsI :: Interval
natsI = I 0 Omega

-- | Construct an open range [n,omega].
fromI :: NatO -> Interval
fromI n = I n Omega

-- | The empty interval.
emptyI :: Interval
emptyI = I 1 0

-- | The interval which contains only omega.
omegaI :: Interval
omegaI = I Omega Omega