{-# language CPP #-} {-# language RankNTypes #-} {-# language PatternGuards #-} #if __GLASGOW_HASKELL__ >= 710 {-# language ViewPatterns #-} {-# language PatternSynonyms #-} #endif -------------------------------------------------------------------------------- -- | -- Module : Numeric.Natural.Lens -- Copyright : (C) 2017 Edward Kmett -- License : BSD-style (see the file LICENSE) -- Maintainer : Edward Kmett -- Stability : provisional -- Portability : portable -- -- Useful tools for GĂ¶del numbering. ------------------------------------------------------------------------------- module Numeric.Natural.Lens ( _Pair , _Sum , _Naturals #if __GLASGOW_HASKELL__ >= 710 , pattern Pair , pattern Sum , pattern Naturals #endif ) where import Control.Lens import Numeric.Natural -- | The natural numbers are isomorphic to the product of the natural numbers with itself. -- -- @N = N*N@ _Pair :: Iso' Natural (Natural, Natural) _Pair = iso hither (uncurry yon) where yon 0 0 = 0 yon m n = case quotRem m 2 of (q,r) -> r + 2 * yon n q -- rotation hither 0 = (0,0) hither n = case quotRem n 2 of (p,r) -> case hither p of (x,y) -> (r+2*y,x) -- rotation -- | The natural numbers are isomorphic to disjoint sums of natural numbers embedded as -- evens or odds. -- -- @N = 2*N@ _Sum :: Iso' Natural (Either Natural Natural) _Sum = iso hither yon where hither p = case quotRem p 2 of (q,0) -> Left q (q,1) -> Right q _ -> error "_Sum: impossible" yon (Left q) = 2*q yon (Right q) = 2*q+1 -- | The natural numbers are isomorphic to lists of natural numbers _Naturals :: Iso' Natural [Natural] _Naturals = iso hither yon where hither 0 = [] hither n | (h, t) <- (n-1)^._Pair = h : hither t yon [] = 0 yon (x:xs) = 1 + review _Pair (x, yon xs) #if __GLASGOW_HASKELL__ >= 710 -- | -- interleaves the bits of two natural numbers pattern Pair :: Natural -> Natural -> Natural pattern Pair x y <- (view _Pair -> (x,y)) where Pair x y = review _Pair (x,y) -- | -- @ -- Sum (Left q) = 2*q -- Sum (Right q) = 2*q+1 -- @ pattern Sum :: Either Natural Natural -> Natural pattern Sum s <- (view _Sum -> s) where Sum s = review _Sum s -- | -- @ -- Naturals [] = 0 -- Naturals (h:t) = 1 + Pair h (Naturals t) -- @ pattern Naturals :: [Natural] -> Natural pattern Naturals xs <- (view _Naturals -> xs) where Naturals xs = review _Naturals xs #endif