-- | 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
[SNat n] -> ShowS
SNat n -> String
(Int -> SNat n -> ShowS)
-> (SNat n -> String) -> ([SNat n] -> ShowS) -> Show (SNat n)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat). Int -> SNat n -> ShowS
forall (n :: Nat). [SNat n] -> ShowS
forall (n :: Nat). SNat n -> String
showList :: [SNat n] -> ShowS
$cshowList :: forall (n :: Nat). [SNat n] -> ShowS
show :: SNat n -> String
$cshow :: forall (n :: Nat). SNat n -> String
showsPrec :: Int -> SNat n -> ShowS
$cshowsPrec :: forall (n :: Nat). Int -> SNat n -> ShowS
Show

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

fromSNat :: SNat n -> Integer
fromSNat :: SNat n -> Integer
fromSNat (SNat Integer
n) = Integer
n

proxyToSNat :: KnownNat n => Proxy n -> SNat n
proxyToSNat :: Proxy n -> SNat n
proxyToSNat Proxy n
proxy = Integer -> SNat n
forall (n :: Nat). Integer -> SNat n
SNat (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
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 :: Integer -> SNat n
unsafeSNat = Integer -> SNat n
forall (n :: Nat). Integer -> SNat n
SNat 

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

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

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

fromSNat64 :: SNat64 n -> Word64
fromSNat64 :: SNat64 n -> Word64
fromSNat64 (SNat64 Word64
n) = Word64
n

proxyToSNat64 :: KnownNat n => Proxy n -> SNat64 n
proxyToSNat64 :: Proxy n -> SNat64 n
proxyToSNat64 Proxy n
proxy = Word64 -> SNat64 n
forall (n :: Nat). Word64 -> SNat64 n
SNat64 (Natural -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
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 :: Word64 -> SNat64 n
unsafeSNat64 = Word64 -> SNat64 n
forall (n :: Nat). 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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = String -> SomeSNat
forall a. HasCallStack => String -> a
error String
"someSNat: expecting a nonnegative number"
  | Bool
otherwise = case Natural -> SomeNat
someNatVal (Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n) of
      SomeNat Proxy n
proxy -> SNat n -> SomeSNat
forall (n :: Nat). KnownNat n => SNat n -> SomeSNat
SomeSNat (Proxy n -> SNat n
forall (n :: Nat). 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 Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
< Int64
0     = String -> SomeSNat64
forall a. HasCallStack => String -> a
error String
"someSNat64: expecting a nonnegative number"
  | Bool
otherwise = case Natural -> SomeNat
someNatVal (Int64 -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int64
n) of
      SomeNat Proxy n
proxy -> SNat64 n -> SomeSNat64
forall (n :: Nat). KnownNat n => SNat64 n -> SomeSNat64
SomeSNat64 (Proxy n -> SNat64 n
forall (n :: Nat). KnownNat n => Proxy n -> SNat64 n
proxyToSNat64 Proxy n
proxy)

someSNat64_ :: Word64 -> SomeSNat64
someSNat64_ :: Word64 -> SomeSNat64
someSNat64_ Word64
n = case Natural -> SomeNat
someNatVal (Word64 -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n) of
  SomeNat Proxy n
proxy -> SNat64 n -> SomeSNat64
forall (n :: Nat). KnownNat n => SNat64 n -> SomeSNat64
SomeSNat64 (Proxy n -> SNat64 n
forall (n :: Nat). 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 :: 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 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
1    = f 1 -> f n
forall a b. a -> b
Unsafe.unsafeCoerce (SNat64 1 -> f 1
thenBranch (Word64 -> SNat64 1
forall (n :: Nat). 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 , Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (SNat n -> Proxy n
forall (n :: Nat). SNat n -> Proxy n
proxyOfSNat SNat n
snat) ) of
    (SNat Integer
value , Natural
tyval) -> String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
value String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
tyval String -> ShowS
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 , Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (SNat64 n -> Proxy n
forall (n :: Nat). SNat64 n -> Proxy n
proxyOfSNat64 SNat64 n
snat) ) of
    (SNat64 Word64
value , Natural
tyval) -> String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. Show a => a -> String
show Word64
value String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
tyval String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"


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