{-# LANGUAGE RankNTypes #-}

-- | <http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/ Constructive gem: double exponentials>

module Cantor
  ( _Natural
  ) where

import Control.Monad.Hyper
import Data.Profunctor
import Numeric.Natural

type Cantor = Natural -> Bool
type Functional = Cantor -> Bool

-- | <http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ Seemingly impossible functional programs>
find :: Functional -> Cantor
find p = branch x0 l0 (find (\r -> p (branch x0 l0 r))) where
  x0 = forsome (\l -> forsome (\r -> p (branch True l r)))
  l0 = find (\l -> forsome (\r -> p (branch x0 l r)))
  branch x _ _ 0 = x
  branch _ l r n
    | odd n = l ((n - 1) `div` 2)
    | otherwise = r ((n - 2) `div` 2)

forevery, forsome :: Functional -> Bool
forsome f = f (find f)
forevery f = not (forsome (not . f))

type Iso' s a = forall p f. (Profunctor p, Functor f) => p a (f a) -> p s (f s)

-- | Inductive Hyper functions from Bool to Bool are isomorphic to the natural numbers.
_Natural :: Iso' Natural (Hyper Bool Bool)
_Natural = dimap (ana enum) (fmap (cata denum)) where

  unpair :: Natural -> (Natural, Natural)
  unpair 0 = (0, 0)
  unpair n = (xr + 2*x, yr + 2*y) where
    (p, xr) = divMod n 2
    (q, yr) = divMod p 2
    (x, y) = unpair q

  enum :: Natural -> Functional
  enum 0 = const False
  enum 1 = const True
  enum n0 = fn' (n0-2) where
    fn' f a = compute 0 f where
      compute k 0 = not (a k)
      compute k 1 = a k
      compute k n | n' <- n - 2, q <- div n' 5 = case mod n' 5 of
        0 -> not (a k) && compute (k+1) q
        1 -> a k       && compute (k+1) q
        2 -> not (a k) || compute (k+1) q
        3 -> a k       || compute (k+1) q
        4 | (x, y) <- unpair q -> if a k
           then compute (k+1) y
           else compute (k+1) x

  pair :: Natural -> Natural -> Natural
  pair 0 0 = 0
  pair m n = mr + 2 * nr + 4 * pair mq nq where
    (mq, mr) = divMod m 2
    (nq, nr) = divMod n 2

  shift :: Bool -> Functional -> Functional
  shift b f = f . prepend b
    prepend b _ 0 = b
    prepend _ a n = a (n-1)

  getConst :: Functional -> Maybe Bool
  getConst f
    | forevery (\a -> f a == b) = Just b
    | otherwise = Nothing
    where b = f (const False)

  denum :: Functional -> Natural
  denum f0 = case getConst f0 of
    Just False -> 0
    Just True -> 1
    Nothing -> 2 + go f0 where
      go f
        | a <- shift False f
        , b <- shift True f = case getConst a of
        Nothing -> case getConst b of
          Nothing -> 6 + 5 * pair (go a) (go b)
          Just False -> 2 + 5 * go a
          Just True -> 5 + 5 * go a
        Just False -> case getConst b of
          Nothing -> 3 + 5 * go b
          Just False -> error "impossible"
          Just True -> 1
        Just True -> case getConst b of
          Nothing -> 4 + 5 * go b
          Just False -> 0
          Just True -> error "impossible"