    {-# language RankNTypes #-}
    {-# language PatternGuards #-}
    {-# language ViewPatterns #-}
    {-# language PatternSynonyms #-}
    --------------------------------------------------------------------------------
    -- |
    -- Module      :  Numeric.Natural.Lens
    -- Copyright   :  (C) 2017 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  provisional
    -- Portability :  portable
    --
    -- Useful tools for Gödel numbering.
    -------------------------------------------------------------------------------
    module Numeric.Natural.Lens
      ( _Pair
      , _Sum
      , _Naturals
      , pattern Pair
      , pattern Sum
      , pattern Naturals
      ) 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' Natural (Natural, Natural)
    _Pair = (Natural -> (Natural, Natural))
    -> ((Natural, Natural) -> Natural)
    -> Iso' Natural (Natural, Natural)
    forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
    iso Natural -> (Natural, Natural)
    forall {b}. Integral b => b -> (b, b)
    hither ((Natural -> Natural -> Natural) -> (Natural, Natural) -> Natural
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Natural -> Natural -> Natural
    forall {t}. Integral t => t -> t -> t
    yon) where
      yon :: t -> t -> t
    yon t
    0 t
    0 = t
    0
      yon t
    m t
    n = case t -> t -> (t, t)
    forall a. Integral a => a -> a -> (a, a)
    quotRem t
    m t
    2 of
        (t
    q,t
    r) -> t
    r t -> t -> t
    forall a. Num a => a -> a -> a
    + t
    2 t -> t -> t
    forall a. Num a => a -> a -> a
    * t -> t -> t
    yon t
    n t
    q -- rotation

      hither :: b -> (b, b)
    hither b
    0 = (b
    0,b
    0)
      hither b
    n = case b -> b -> (b, b)
    forall a. Integral a => a -> a -> (a, a)
    quotRem b
    n b
    2 of
       (b
    p,b
    r) -> case b -> (b, b)
    hither b
    p of
         (b
    x,b
    y) -> (b
    rb -> b -> b
    forall a. Num a => a -> a -> a
    +b
    2b -> b -> b
    forall a. Num a => a -> a -> a
    *b
    y,b
    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' Natural (Either Natural Natural)
    _Sum = (Natural -> Either Natural Natural)
    -> (Either Natural Natural -> Natural)
    -> Iso' Natural (Either Natural Natural)
    forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
    iso Natural -> Either Natural Natural
    forall {b}. Integral b => b -> Either b b
    hither Either Natural Natural -> Natural
    forall {a}. Num a => Either a a -> a
    yon where
      hither :: b -> Either b b
    hither b
    p = case b -> b -> (b, b)
    forall a. Integral a => a -> a -> (a, a)
    quotRem b
    p b
    2 of
        (b
    q,b
    0) -> b -> Either b b
    forall a b. a -> Either a b
    Left b
    q
        (b
    q,b
    1) -> b -> Either b b
    forall a b. b -> Either a b
    Right b
    q
        (b, b)
    _     -> [Char] -> Either b b
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "_Sum: impossible"
      yon :: Either a a -> a
    yon (Left a
    q)  = a
    2a -> a -> a
    forall a. Num a => a -> a -> a
    *a
    q
      yon (Right a
    q) = a
    2a -> a -> a
    forall a. Num a => a -> a -> a
    *a
    qa -> a -> a
    forall a. Num a => a -> a -> a
    +a
    1

    -- | The natural numbers are isomorphic to lists of natural numbers
    _Naturals :: Iso' Natural [Natural]
    _Naturals :: Iso' Natural [Natural]
    _Naturals = (Natural -> [Natural])
    -> ([Natural] -> Natural) -> Iso' Natural [Natural]
    forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
    iso Natural -> [Natural]
    hither [Natural] -> Natural
    yon where
      hither :: Natural -> [Natural]
    hither Natural
    0 = []
      hither Natural
    n | (Natural
    h, Natural
    t) <- (Natural
    nNatural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    -Natural
    1)Natural
    -> Getting (Natural, Natural) Natural (Natural, Natural)
    -> (Natural, Natural)
    forall s a. s -> Getting a s a -> a
    ^.Getting (Natural, Natural) Natural (Natural, Natural)
    Iso' Natural (Natural, Natural)
    _Pair = Natural
    h Natural -> [Natural] -> [Natural]
    forall a. a -> [a] -> [a]
    : Natural -> [Natural]
    hither Natural
    t
      yon :: [Natural] -> Natural
    yon [] = Natural
    0
      yon (Natural
    x:[Natural]
    xs) = Natural
    1 Natural -> Natural -> Natural
    forall a. Num a => a -> a -> a
    + AReview Natural (Natural, Natural) -> (Natural, Natural) -> Natural
    forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
    review AReview Natural (Natural, Natural)
    Iso' Natural (Natural, Natural)
    _Pair (Natural
    x, [Natural] -> Natural
    yon [Natural]
    xs)

    -- |
    -- interleaves the bits of two natural numbers
    pattern Pair :: Natural -> Natural -> Natural
    pattern $mPair :: forall {r}.
    Natural -> (Natural -> Natural -> r) -> ((# #) -> r) -> r
    $bPair :: Natural -> Natural -> Natural
    Pair x y <- (view _Pair -> (x,y)) where
      Pair Natural
    x Natural
    y = AReview Natural (Natural, Natural) -> (Natural, Natural) -> Natural
    forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
    review AReview Natural (Natural, Natural)
    Iso' Natural (Natural, Natural)
    _Pair (Natural
    x,Natural
    y)

    -- |
    -- @
    -- Sum (Left q) = 2*q
    -- Sum (Right q) = 2*q+1
    -- @
    pattern Sum :: Either Natural Natural -> Natural
    pattern $mSum :: forall {r}.
    Natural -> (Either Natural Natural -> r) -> ((# #) -> r) -> r
    $bSum :: Either Natural Natural -> Natural
    Sum s <- (view _Sum -> s) where
      Sum Either Natural Natural
    s = AReview Natural (Either Natural Natural)
    -> Either Natural Natural -> Natural
    forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
    review AReview Natural (Either Natural Natural)
    Iso' Natural (Either Natural Natural)
    _Sum Either Natural Natural
    s

    -- |
    -- @
    -- Naturals [] = 0
    -- Naturals (h:t) = 1 + Pair h (Naturals t)
    -- @
    pattern Naturals :: [Natural] -> Natural
    pattern $mNaturals :: forall {r}. Natural -> ([Natural] -> r) -> ((# #) -> r) -> r
    $bNaturals :: [Natural] -> Natural
    Naturals xs <- (view _Naturals -> xs) where
      Naturals [Natural]
    xs = AReview Natural [Natural] -> [Natural] -> Natural
    forall b (m :: * -> *) t. MonadReader b m => AReview t b -> m t
    review AReview Natural [Natural]
    Iso' Natural [Natural]
    _Naturals [Natural]
    xs