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
- data NatO
- omega :: NatO
- natO :: (Integer -> a) -> a -> NatO -> a
- data Interval
- iLow :: Interval -> NatO
- iHigh :: Interval -> NatO
- decrI :: Interval -> Interval
- union :: Interval -> Interval -> Interval
- intersect :: Interval -> Interval -> Interval
- elem :: Integer -> Interval -> Bool
- toList :: Interval -> [Integer]
- natsI :: Interval
- fromI :: NatO -> Interval
- emptyI :: Interval
- omegaI :: Interval
NatO is an explicit representation of the co-inductive Nat type
which admits an infinite value, omega. Our intuition for the
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.
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.
The union of two intervals is the smallest interval containing both.
The intersection of two intervals is the largest interval contained in both.