{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
module Type.Data.Num.Unary (
    Unary, unary, Un, Zero, Succ, zero, succ,
    HeadSingleton(Zero, Succ), headSingleton,
    Singleton(..), singleton, singletonFromProxy,
    integerFromSingleton, integralFromSingleton,
    integralFromProxy,
    Natural(..), Positive(..),
    (:+:), (:*:),
    reifyNatural,
    ) where

import qualified Type.Data.Num as Num
import qualified Type.Base.Proxy as Proxy
import Type.Base.Proxy (Proxy(Proxy))

import Text.Printf (printf)

import Prelude hiding (succ)


-- | Representation name for unary type level numbers.
data Unary

data Un x
data Zero
data Succ x
{-
Negative numbers could be represented by Pred
but this would complicate our proofs.
We would require that a number contains only Succ or Pred.
Alternative:
Int = Zero | Neg Nat | Pos Nat
Nat = None | Succ Nat
-}

zero :: Proxy Zero
zero :: Proxy Zero
zero = Proxy Zero
forall a. Proxy a
Proxy

succ :: Proxy n -> Proxy (Succ n)
succ :: Proxy n -> Proxy (Succ n)
succ Proxy n
Proxy = Proxy (Succ n)
forall a. Proxy a
Proxy


class Natural n where
    switchNat ::
        f Zero ->
        (forall m. (Natural m) => f (Succ m)) ->
        f n

instance Natural Zero where switchNat :: f Zero -> (forall m. Natural m => f (Succ m)) -> f Zero
switchNat f Zero
x forall m. Natural m => f (Succ m)
_ = f Zero
x
instance Natural n => Natural (Succ n) where switchNat :: f Zero -> (forall m. Natural m => f (Succ m)) -> f (Succ n)
switchNat f Zero
_ forall m. Natural m => f (Succ m)
x = f (Succ n)
forall m. Natural m => f (Succ m)
x


class (Natural n) => Positive n where
    switchPos ::
        (forall m. (Natural m) => f (Succ m)) ->
        f n

instance Natural n => Positive (Succ n) where switchPos :: (forall m. Natural m => f (Succ m)) -> f (Succ n)
switchPos forall m. Natural m => f (Succ m)
x = f (Succ n)
forall m. Natural m => f (Succ m)
x


type family x :+: y
type instance x :+: Zero = x
type instance x :+: Succ y = Succ (x :+: y)

type family x :*: y
type instance _x :*: Zero = Zero
type instance x :*: Succ y = x :+: (x :*: y)



data HeadSingleton n where
    Zero :: HeadSingleton Zero
    Succ :: (Natural n) => HeadSingleton (Succ n)

headSingleton :: (Natural n) => HeadSingleton n
headSingleton :: HeadSingleton n
headSingleton = HeadSingleton Zero
-> (forall m. Natural m => HeadSingleton (Succ m))
-> HeadSingleton n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat HeadSingleton Zero
Zero forall m. Natural m => HeadSingleton (Succ m)
Succ


newtype Singleton n = Singleton Integer

instance (Natural n) => Num.Integer (Un n) where
    singleton :: Singleton (Un n)
singleton = Singleton n -> Singleton (Un n)
forall n. Singleton n -> Singleton (Un n)
singletonToGeneric Singleton n
forall n. Natural n => Singleton n
singleton
    type Repr (Un n) = Unary

singletonToGeneric :: Singleton n -> Num.Singleton (Un n)
singletonToGeneric :: Singleton n -> Singleton (Un n)
singletonToGeneric (Singleton Integer
n) = Integer -> Singleton (Un n)
forall d. Integer -> Singleton d
Num.Singleton Integer
n

singleton :: (Natural n) => Singleton n
singleton :: Singleton n
singleton =
    Singleton Zero
-> (forall m. Natural m => Singleton (Succ m)) -> Singleton n
forall n (f :: * -> *).
Natural n =>
f Zero -> (forall m. Natural m => f (Succ m)) -> f n
switchNat
        (Integer -> Singleton Zero
forall n. Integer -> Singleton n
Singleton Integer
0)
        (Singleton m -> Singleton (Succ m)
forall n. Natural n => Singleton n -> Singleton (Succ n)
succSingleton Singleton m
forall n. Natural n => Singleton n
singleton)

succSingleton ::
    (Natural n) =>
    Singleton n -> Singleton (Succ n)
succSingleton :: Singleton n -> Singleton (Succ n)
succSingleton (Singleton Integer
n) = Integer -> Singleton (Succ n)
forall n. Integer -> Singleton n
Singleton (Integer -> Singleton (Succ n)) -> Integer -> Singleton (Succ n)
forall a b. (a -> b) -> a -> b
$ Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1


integerFromSingleton :: (Natural n) => Singleton n -> Integer
integerFromSingleton :: Singleton n -> Integer
integerFromSingleton (Singleton Integer
n) = Integer
n

integralFromSingleton :: (Natural n, Num a) => Singleton n -> a
integralFromSingleton :: Singleton n -> a
integralFromSingleton = Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> (Singleton n -> Integer) -> Singleton n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Singleton n -> Integer
forall n. Natural n => Singleton n -> Integer
integerFromSingleton

singletonFromProxy :: (Natural n) => Proxy n -> Singleton n
singletonFromProxy :: Proxy n -> Singleton n
singletonFromProxy Proxy n
Proxy = Singleton n
forall n. Natural n => Singleton n
singleton

integralFromProxy :: (Natural n, Num a) => Proxy n -> a
integralFromProxy :: Proxy n -> a
integralFromProxy = Singleton n -> a
forall n a. (Natural n, Num a) => Singleton n -> a
integralFromSingleton (Singleton n -> a) -> (Proxy n -> Singleton n) -> Proxy n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy n -> Singleton n
forall n. Natural n => Proxy n -> Singleton n
singletonFromProxy


instance Num.Representation Unary where
    reifyIntegral :: Proxy Unary
-> Integer
-> (forall s. (Integer s, Repr s ~ Unary) => Proxy s -> a)
-> a
reifyIntegral Proxy Unary
_ Integer
i forall s. (Integer s, Repr s ~ Unary) => Proxy s -> a
k = Integer -> (forall s. Natural s => Proxy s -> a) -> a
forall w. Integer -> (forall s. Natural s => Proxy s -> w) -> w
reifyIntegral Integer
i (Proxy (Un s) -> a
forall s. (Integer s, Repr s ~ Unary) => Proxy s -> a
k (Proxy (Un s) -> a) -> (Proxy s -> Proxy (Un s)) -> Proxy s -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> Proxy (Un s)
forall n. Proxy n -> Proxy (Un n)
unary)

unary :: Proxy n -> Proxy (Un n)
unary :: Proxy n -> Proxy (Un n)
unary Proxy n
Proxy = Proxy (Un n)
forall a. Proxy a
Proxy

stripUn :: Proxy (Un n) -> Proxy n
stripUn :: Proxy (Un n) -> Proxy n
stripUn Proxy (Un n)
Proxy = Proxy n
forall a. Proxy a
Proxy

reifyIntegral :: Integer -> (forall s. Natural s => Proxy s -> w) -> w
reifyIntegral :: Integer -> (forall s. Natural s => Proxy s -> w) -> w
reifyIntegral Integer
n forall s. Natural s => Proxy s -> w
f =
    if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
      then [Char] -> w
forall a. HasCallStack => [Char] -> a
error [Char]
"negative unary numbers not supported so far"
      else Integer -> (forall s. Natural s => Proxy s -> w) -> w
forall w. Integer -> (forall s. Natural s => Proxy s -> w) -> w
reifyNatural Integer
n forall s. Natural s => Proxy s -> w
f

reifyNatural :: Integer -> (forall s. Natural s => Proxy s -> w) -> w
reifyNatural :: Integer -> (forall s. Natural s => Proxy s -> w) -> w
reifyNatural Integer
n forall s. Natural s => Proxy s -> w
f =
   if Integer
nInteger -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
0
     then Integer -> (forall s. Natural s => Proxy s -> w) -> w
forall w. Integer -> (forall s. Natural s => Proxy s -> w) -> w
reifyNatural (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) (Proxy (Succ s) -> w
forall s. Natural s => Proxy s -> w
f (Proxy (Succ s) -> w)
-> (Proxy s -> Proxy (Succ s)) -> Proxy s -> w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> Proxy (Succ s)
forall n. Proxy n -> Proxy (Succ n)
succ)
     else Proxy Zero -> w
forall s. Natural s => Proxy s -> w
f Proxy Zero
zero


type instance Un x Num.:+: Un y = Un (x :+: y)
type instance Un x Num.:*: Un y = Un (x :*: y)


instance Natural a => Proxy.Show (Un a) where
   showsPrec :: Int -> Proxy (Un a) -> ShowS
showsPrec Int
prec =
      (\Integer
n -> Bool -> ShowS -> ShowS
showParen (Int
precInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
10) ([Char] -> ShowS
showString ([Char] -> Integer -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"unary u%d" Integer
n)))
       (Integer -> ShowS)
-> (Proxy (Un a) -> Integer) -> Proxy (Un a) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Singleton a -> Integer
forall n. Natural n => Singleton n -> Integer
integerFromSingleton (Singleton a -> Integer)
-> (Proxy (Un a) -> Singleton a) -> Proxy (Un a) -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy a -> Singleton a
forall n. Natural n => Proxy n -> Singleton n
singletonFromProxy (Proxy a -> Singleton a)
-> (Proxy (Un a) -> Proxy a) -> Proxy (Un a) -> Singleton a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Un a) -> Proxy a
forall n. Proxy (Un n) -> Proxy n
stripUn