{-# LANGUAGE CPP #-}

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
#if __GLASGOW_HASKELL__ >= 904
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE ViewPatterns #-}
#endif

-- | A facility for faking GADTs that work sufficiently similarly
-- to unary natural numbers.
module Nattish
  ( Nattish (Zeroy, Succy)
  )
  where
import Unsafe.Coerce (unsafeCoerce)
#if __GLASGOW_HASKELL__ >= 800
import Data.Kind (Type)
#endif

-- | Conceptually,
--
-- @
-- data Nattish :: forall k. k -> (k -> k) -> k -> Type where
--   Zeroy :: Nattish zero succ zero
--   Succy :: !(Nattish zero succ n) -> Nattish zero succ (succ n)
-- @
--
-- This abstracts over the zero and successor constructors, so it can be used
-- in any sufficiently Nat-like context. In our case, we can use it for the @Zero@
-- and @Succ@ constructors of both @MinQueue@ and @MinPQueue@. With recent
-- versions of GHC, @Nattish@ is actually represented as a machine integer, so
-- it is very fast to work with.

#if __GLASGOW_HASKELL__ < 904
data Nattish :: k -> (k -> k) -> k -> * where
  Zeroy :: Nattish zero succ zero
  Succy :: !(Nattish zero succ n) -> Nattish zero succ (succ n)

toWord :: Nattish zero succ n -> Word
toWord = go 0
  where
    go :: Word -> Nattish zero succ n -> Word
    go !acc Zeroy = acc
    go !acc (Succy n) = go (acc + 1) n

instance Show (Nattish zero succ n) where
  showsPrec p n = showParen (p > 10) $
    showString "Nattish " . showsPrec 11 (toWord n)
#else

type Nattish :: forall k. k -> (k -> k) -> k -> Type
newtype Nattish zero succ n = Nattish Word
  deriving (Int -> Nattish zero succ n -> ShowS
[Nattish zero succ n] -> ShowS
Nattish zero succ n -> String
(Int -> Nattish zero succ n -> ShowS)
-> (Nattish zero succ n -> String)
-> ([Nattish zero succ n] -> ShowS)
-> Show (Nattish zero succ n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (zero :: k) (succ :: k -> k) (n :: k).
Int -> Nattish zero succ n -> ShowS
forall k (zero :: k) (succ :: k -> k) (n :: k).
[Nattish zero succ n] -> ShowS
forall k (zero :: k) (succ :: k -> k) (n :: k).
Nattish zero succ n -> String
$cshowsPrec :: forall k (zero :: k) (succ :: k -> k) (n :: k).
Int -> Nattish zero succ n -> ShowS
showsPrec :: Int -> Nattish zero succ n -> ShowS
$cshow :: forall k (zero :: k) (succ :: k -> k) (n :: k).
Nattish zero succ n -> String
show :: Nattish zero succ n -> String
$cshowList :: forall k (zero :: k) (succ :: k -> k) (n :: k).
[Nattish zero succ n] -> ShowS
showList :: [Nattish zero succ n] -> ShowS
Show)
type role Nattish nominal nominal nominal

data Res zero succ n where
  ResZero :: Res zero succ zero
  ResSucc :: !(Nattish zero succ n) -> Res zero succ (succ n)

check :: Nattish zero succ n -> Res zero succ n
check :: forall {k} (zero :: k) (succ :: k -> k) (n :: k).
Nattish zero succ n -> Res zero succ n
check (Nattish Word
0) = Res Any Any Any -> Res zero succ n
forall a b. a -> b
unsafeCoerce Res Any Any Any
forall {k} (zero :: k) (succ :: k -> k). Res zero succ zero
ResZero
check (Nattish Word
n) = Res Any Any (Any Any) -> Res zero succ n
forall a b. a -> b
unsafeCoerce (Res Any Any (Any Any) -> Res zero succ n)
-> Res Any Any (Any Any) -> Res zero succ n
forall a b. (a -> b) -> a -> b
$ Nattish Any Any Any -> Res Any Any (Any Any)
forall {k} (zero :: k) (succ :: k -> k) (n :: k).
Nattish zero succ n -> Res zero succ (succ n)
ResSucc (Word -> Nattish Any Any Any
forall k (zero :: k) (succ :: k -> k) (n :: k).
Word -> Nattish zero succ n
Nattish (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1))

pattern Zeroy :: forall {k} zero succ (n :: k). () => n ~ zero => Nattish zero succ n
pattern $mZeroy :: forall {r} {k} {zero :: k} {succ :: k -> k} {n :: k}.
Nattish zero succ n -> ((n ~ zero) => r) -> ((# #) -> r) -> r
$bZeroy :: forall {k} (zero :: k) (succ :: k -> k) (n :: k).
(n ~ zero) =>
Nattish zero succ n
Zeroy <- (check -> ResZero)
  where
    Zeroy = Word -> Nattish zero succ n
forall k (zero :: k) (succ :: k -> k) (n :: k).
Word -> Nattish zero succ n
Nattish Word
0
{-# INLINE Zeroy #-}

pattern Succy :: forall {k} zero succ (n :: k). () => forall (n' :: k). n ~ succ n' => Nattish zero succ n' -> Nattish zero succ n
pattern $mSuccy :: forall {r} {k} {zero :: k} {succ :: k -> k} {n :: k}.
Nattish zero succ n
-> (forall {n' :: k}. (n ~ succ n') => Nattish zero succ n' -> r)
-> ((# #) -> r)
-> r
$bSuccy :: forall {k} (zero :: k) (succ :: k -> k) (n :: k) (n' :: k).
(n ~ succ n') =>
Nattish zero succ n' -> Nattish zero succ n
Succy n <- (check -> ResSucc n)
  where
    Succy (Nattish Word
n) = Word -> Nattish zero succ n
forall k (zero :: k) (succ :: k -> k) (n :: k).
Word -> Nattish zero succ n
Nattish (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1)
{-# INLINE Succy #-}

{-# COMPLETE Zeroy, Succy #-}

#endif