-- | Singleton types.
--
-- This is a separate (internal) module, because sometimes we need to create 
-- singletons in other modules than "Math.FiniteField.TypeLevel"
--

{-# LANGUAGE DataKinds, KindSignatures, GADTs, ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}

module Math.FiniteField.TypeLevel.Singleton where

--------------------------------------------------------------------------------

import Data.Int
import Data.Word

import GHC.TypeNats
import Data.Proxy

import Unsafe.Coerce as Unsafe

--------------------------------------------------------------------------------
-- * Singleton types

-- | Nat-singletons
newtype SNat (n :: Nat) 
  = SNat Integer
  deriving Int -> SNat n -> ShowS
forall (n :: Natural). Int -> SNat n -> ShowS
forall (n :: Natural). [SNat n] -> ShowS
forall (n :: Natural). SNat n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SNat n] -> ShowS
$cshowList :: forall (n :: Natural). [SNat n] -> ShowS
show :: SNat n -> String
$cshow :: forall (n :: Natural). SNat n -> String
showsPrec :: Int -> SNat n -> ShowS
$cshowsPrec :: forall (n :: Natural). Int -> SNat n -> ShowS
Show

proxyOfSNat :: SNat n -> Proxy n
proxyOfSNat :: forall (n :: Natural). SNat n -> Proxy n
proxyOfSNat SNat n
_ = forall {k} (t :: k). Proxy t
Proxy

fromSNat :: SNat n -> Integer
fromSNat :: forall (n :: Natural). SNat n -> Integer
fromSNat (SNat Integer
n) = Integer
n

proxyToSNat :: KnownNat n => Proxy n -> SNat n
proxyToSNat :: forall (n :: Natural). KnownNat n => Proxy n -> SNat n
proxyToSNat Proxy n
proxy = forall (n :: Natural). Integer -> SNat n
SNat (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
proxy))

-- | You are responsible here! 
--
-- (this is exported primarily because the testsuite is much simpler using this...)
--
unsafeSNat :: Integer -> SNat n
unsafeSNat :: forall (n :: Natural). Integer -> SNat n
unsafeSNat = forall (n :: Natural). Integer -> SNat n
SNat 

--------------------------------------------------------------------------------

-- | Word-sized nat-singletons
newtype SNat64 (n :: Nat) 
  = SNat64 Word64
  deriving Int -> SNat64 n -> ShowS
forall (n :: Natural). Int -> SNat64 n -> ShowS
forall (n :: Natural). [SNat64 n] -> ShowS
forall (n :: Natural). SNat64 n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SNat64 n] -> ShowS
$cshowList :: forall (n :: Natural). [SNat64 n] -> ShowS
show :: SNat64 n -> String
$cshow :: forall (n :: Natural). SNat64 n -> String
showsPrec :: Int -> SNat64 n -> ShowS
$cshowsPrec :: forall (n :: Natural). Int -> SNat64 n -> ShowS
Show

proxyOfSNat64 :: SNat64 n -> Proxy n
proxyOfSNat64 :: forall (n :: Natural). SNat64 n -> Proxy n
proxyOfSNat64 SNat64 n
_ = forall {k} (t :: k). Proxy t
Proxy

fromSNat64 :: SNat64 n -> Word64
fromSNat64 :: forall (n :: Natural). SNat64 n -> Word64
fromSNat64 (SNat64 Word64
n) = Word64
n

proxyToSNat64 :: KnownNat n => Proxy n -> SNat64 n
proxyToSNat64 :: forall (n :: Natural). KnownNat n => Proxy n -> SNat64 n
proxyToSNat64 Proxy n
proxy = forall (n :: Natural). Word64 -> SNat64 n
SNat64 (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
proxy))

-- | You are responsible here! 
--
-- (this is exported primarily because the testsuite is much simpler using this...)
--
unsafeSNat64 :: Word64 -> SNat64 n
unsafeSNat64 :: forall (n :: Natural). Word64 -> SNat64 n
unsafeSNat64 = forall (n :: Natural). Word64 -> SNat64 n
SNat64 

--------------------------------------------------------------------------------
-- * Creating singleton types

data SomeSNat 
  = forall (n :: Nat). KnownNat n => SomeSNat (SNat n)

deriving instance Show SomeSNat

someSNat :: Integer -> SomeSNat
someSNat :: Integer -> SomeSNat
someSNat Integer
n 
  | Integer
n forall a. Ord a => a -> a -> Bool
< Integer
0     = forall a. HasCallStack => String -> a
error String
"someSNat: expecting a nonnegative number"
  | Bool
otherwise = case Natural -> SomeNat
someNatVal (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n) of
      SomeNat Proxy n
proxy -> forall (n :: Natural). KnownNat n => SNat n -> SomeSNat
SomeSNat (forall (n :: Natural). KnownNat n => Proxy n -> SNat n
proxyToSNat Proxy n
proxy)

data SomeSNat64
  = forall (n :: Nat). KnownNat n => SomeSNat64 (SNat64 n)

deriving instance Show SomeSNat64

someSNat64 :: Int64 -> SomeSNat64
someSNat64 :: Int64 -> SomeSNat64
someSNat64 Int64
n 
  | Int64
n forall a. Ord a => a -> a -> Bool
< Int64
0     = forall a. HasCallStack => String -> a
error String
"someSNat64: expecting a nonnegative number"
  | Bool
otherwise = case Natural -> SomeNat
someNatVal (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
n) of
      SomeNat Proxy n
proxy -> forall (n :: Natural). KnownNat n => SNat64 n -> SomeSNat64
SomeSNat64 (forall (n :: Natural). KnownNat n => Proxy n -> SNat64 n
proxyToSNat64 Proxy n
proxy)

someSNat64_ :: Word64 -> SomeSNat64
someSNat64_ :: Word64 -> SomeSNat64
someSNat64_ Word64
n = case Natural -> SomeNat
someNatVal (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n) of
  SomeNat Proxy n
proxy -> forall (n :: Natural). KnownNat n => SNat64 n -> SomeSNat64
SomeSNat64 (forall (n :: Natural). KnownNat n => Proxy n -> SNat64 n
proxyToSNat64 Proxy n
proxy)

snat64IfOneThenElse :: forall (n :: Nat) (f :: Nat -> *). SNat64 n -> (SNat64 1 -> f 1) -> (SNat64 n -> f n) -> f n
snat64IfOneThenElse :: forall (n :: Natural) (f :: Natural -> *).
SNat64 n -> (SNat64 1 -> f 1) -> (SNat64 n -> f n) -> f n
snat64IfOneThenElse sn :: SNat64 n
sn@(SNat64 Word64
n) SNat64 1 -> f 1
thenBranch SNat64 n -> f n
elseBranch
  | Word64
n forall a. Eq a => a -> a -> Bool
== Word64
1    = forall a b. a -> b
Unsafe.unsafeCoerce (SNat64 1 -> f 1
thenBranch (forall (n :: Natural). Word64 -> SNat64 n
SNat64 Word64
1))
  | Bool
otherwise = SNat64 n -> f n
elseBranch SNat64 n
sn

--------------------------------------------------------------------------------
-- * sanity checking

checkSomeSNat :: SomeSNat -> String
checkSomeSNat :: SomeSNat -> String
checkSomeSNat SomeSNat
some = case SomeSNat
some of
  SomeSNat SNat n
snat -> case ( SNat n
snat , forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (n :: Natural). SNat n -> Proxy n
proxyOfSNat SNat n
snat) ) of
    (SNat Integer
value , Natural
tyval) -> String
"[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
value forall a. [a] -> [a] -> [a]
++ String
"=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Natural
tyval forall a. [a] -> [a] -> [a]
++ String
"]"

checkSomeSNat64 :: SomeSNat64 -> String
checkSomeSNat64 :: SomeSNat64 -> String
checkSomeSNat64 SomeSNat64
some = case SomeSNat64
some of
  SomeSNat64 SNat64 n
snat -> case ( SNat64 n
snat , forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (n :: Natural). SNat64 n -> Proxy n
proxyOfSNat64 SNat64 n
snat) ) of
    (SNat64 Word64
value , Natural
tyval) -> String
"[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Word64
value forall a. [a] -> [a] -> [a]
++ String
"=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Natural
tyval forall a. [a] -> [a] -> [a]
++ String
"]"


--------------------------------------------------------------------------------