{-# 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