-- | Type level naturals, singletons, prime witnesses and stuff.
--
-- This would be much simpler in a dependently typed language;
-- alas, we are in Haskell, so for now we have to feel the pain.
--
-- How to use this, the over-complicated way:
--
-- * create a 'SomeSNat' from an integer using the function 'someSNat'
-- 
-- * pattern match on it with a @case@ expression. Within the matched
--   scope, the type parameter is \"instantiated\". So all your program
--   will be \"inside\" this case branch (of course you can call out
--   to functions)
--
-- * create witnesses for this being prime and\/or being small using
--   the functions 'isPrime' and 'fits31Bits' 
--
-- * if you want small primes, create a \"small prime witness\" using
--   'mkSmallPrime'
--
-- * now you are ready to use the resulting witness (of type @IsPrime n@
--   or @IsSmallPrime n@) to create finite fields.
--
-- Or you can just the functions provided with each field implementation
-- to create the fields directly (in form of existantials, ie. sigma types,
-- so you still have to do the @case _ of@ thing).
--

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

module Math.FiniteField.TypeLevel
  ( -- * Singleton types
    SNat   , fromSNat   , proxyOfSNat   , proxyToSNat   , unsafeSNat
  , SNat64 , fromSNat64 , proxyOfSNat64 , proxyToSNat64 , unsafeSNat64
    -- * Creating singleton types
  , SomeSNat(..) , someSNat , SomeSNat64(..) , someSNat64 , someSNat64_
    -- * Small numbers
  , Fits31Bits , from31Bit , from31BitSigned , from31Bit' , fits31Bits 
    -- * Primes
  , IsPrime , fromPrime , fromPrime' 
  , isPrime , believeMeItsPrime
    -- * Small primes
  , IsSmallPrime , fromSmallPrime , fromSmallPrimeSigned , fromSmallPrimeInteger , fromSmallPrime' 
  , isSmallPrime , believeMeItsASmallPrime
  , smallPrimeIsPrime , smallPrimeIsSmall , mkSmallPrime
    -- * Proxy
  , proxyOf, proxyOf1
    -- * Sanity checking
  , checkSomeSNat , checkSomeSNat64
  ) 
  where

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

import Data.Int
import Data.Word
import Data.Proxy

import GHC.TypeNats
import Data.Proxy

import Math.FiniteField.Primes
import Math.FiniteField.TypeLevel.Singleton

--------------------------------------------------------------------------------
-- * Primes

-- | Prime witness
newtype IsPrime (n :: Nat) where
  PrimeWitness :: SNat n -> IsPrime n

deriving instance Show (IsPrime n)

fromPrime' :: IsPrime n -> SNat n
fromPrime' :: IsPrime n -> SNat n
fromPrime' (PrimeWitness SNat n
sn) = SNat n
sn

fromPrime :: IsPrime n -> Integer
fromPrime :: IsPrime n -> Integer
fromPrime (PrimeWitness SNat n
sn) = SNat n -> Integer
forall (n :: Nat). SNat n -> Integer
fromSNat SNat n
sn

-- | Prime testing.
--
-- Note: this uses trial division at the moment, 
-- so it's only good for small numbers for now
--
isPrime :: SNat n -> Maybe (IsPrime n)
isPrime :: SNat n -> Maybe (IsPrime n)
isPrime SNat n
sn = if (SNat n -> Integer
forall (n :: Nat). SNat n -> Integer
fromSNat SNat n
sn Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1) Bool -> Bool -> Bool
&& Integer -> Bool
isPrimeTrialDivision (SNat n -> Integer
forall (n :: Nat). SNat n -> Integer
fromSNat SNat n
sn)
  then IsPrime n -> Maybe (IsPrime n)
forall a. a -> Maybe a
Just (SNat n -> IsPrime n
forall (n :: Nat). SNat n -> IsPrime n
PrimeWitness SNat n
sn)
  else Maybe (IsPrime n)
forall a. Maybe a
Nothing

-- | Escape hatch
believeMeItsPrime :: SNat n -> IsPrime n
believeMeItsPrime :: SNat n -> IsPrime n
believeMeItsPrime SNat n
sn = SNat n -> IsPrime n
forall (n :: Nat). SNat n -> IsPrime n
PrimeWitness SNat n
sn

--------------------------------------------------------------------------------
-- * Small numbers

newtype Fits31Bits (n :: Nat) where
  Witness31 :: SNat64 n -> Fits31Bits n

deriving instance Show (Fits31Bits n)

from31Bit' :: Fits31Bits n -> SNat64 n
from31Bit' :: Fits31Bits n -> SNat64 n
from31Bit' (Witness31 SNat64 n
sn) = SNat64 n
sn

from31Bit :: Fits31Bits n -> Word64
from31Bit :: Fits31Bits n -> Word64
from31Bit (Witness31 SNat64 n
sn) = SNat64 n -> Word64
forall (n :: Nat). SNat64 n -> Word64
fromSNat64 SNat64 n
sn

from31BitSigned :: Fits31Bits n -> Int64
from31BitSigned :: Fits31Bits n -> Int64
from31BitSigned (Witness31 SNat64 n
sn) = Word64 -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SNat64 n -> Word64
forall (n :: Nat). SNat64 n -> Word64
fromSNat64 SNat64 n
sn)

-- | Creating a witness for a number being small (less than @2^31@)
fits31Bits :: SNat64 n -> Maybe (Fits31Bits n)
fits31Bits :: SNat64 n -> Maybe (Fits31Bits n)
fits31Bits sn :: SNat64 n
sn@(SNat64 Word64
n) 
  | Word64
n Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64
0 Bool -> Bool -> Bool
&& Word64
n Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
< Word64
2Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
31   = Fits31Bits n -> Maybe (Fits31Bits n)
forall a. a -> Maybe a
Just (SNat64 n -> Fits31Bits n
forall (n :: Nat). SNat64 n -> Fits31Bits n
Witness31 SNat64 n
sn)
  | Bool
otherwise            = Maybe (Fits31Bits n)
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- * Small primes

newtype IsSmallPrime (n :: Nat) where
  SmallPrimeWitness :: SNat64 n -> IsSmallPrime n

deriving instance Show (IsSmallPrime n)

fromSmallPrime' :: IsSmallPrime n -> SNat64 n
fromSmallPrime' :: IsSmallPrime n -> SNat64 n
fromSmallPrime' (SmallPrimeWitness SNat64 n
sn) = SNat64 n
sn

fromSmallPrime :: IsSmallPrime n -> Word64
fromSmallPrime :: IsSmallPrime n -> Word64
fromSmallPrime (SmallPrimeWitness SNat64 n
sn) = SNat64 n -> Word64
forall (n :: Nat). SNat64 n -> Word64
fromSNat64 SNat64 n
sn

fromSmallPrimeInteger :: IsSmallPrime n -> Integer
fromSmallPrimeInteger :: IsSmallPrime n -> Integer
fromSmallPrimeInteger (SmallPrimeWitness SNat64 n
sn) = Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SNat64 n -> Word64
forall (n :: Nat). SNat64 n -> Word64
fromSNat64 SNat64 n
sn)

fromSmallPrimeSigned :: IsSmallPrime n -> Int64
fromSmallPrimeSigned :: IsSmallPrime n -> Int64
fromSmallPrimeSigned (SmallPrimeWitness SNat64 n
sn) = Word64 -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SNat64 n -> Word64
forall (n :: Nat). SNat64 n -> Word64
fromSNat64 SNat64 n
sn)

-- | Prime testing.
--
-- Note: this uses trial division at the moment, 
-- so it's only good for small numbers for now
--
isSmallPrime :: SNat64 n -> Maybe (IsSmallPrime n)
isSmallPrime :: SNat64 n -> Maybe (IsSmallPrime n)
isSmallPrime SNat64 n
sn = 
  if (Word64
n Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
1) Bool -> Bool -> Bool
&& (Word64
n Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
< Word64
2Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
31) Bool -> Bool -> Bool
&& Integer -> Bool
isPrimeTrialDivision (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n)
    then IsSmallPrime n -> Maybe (IsSmallPrime n)
forall a. a -> Maybe a
Just (SNat64 n -> IsSmallPrime n
forall (n :: Nat). SNat64 n -> IsSmallPrime n
SmallPrimeWitness SNat64 n
sn)
    else Maybe (IsSmallPrime n)
forall a. Maybe a
Nothing
  where
    n :: Word64
n = SNat64 n -> Word64
forall (n :: Nat). SNat64 n -> Word64
fromSNat64 SNat64 n
sn

smallPrimeIsPrime :: IsSmallPrime n -> IsPrime n
smallPrimeIsPrime :: IsSmallPrime n -> IsPrime n
smallPrimeIsPrime (SmallPrimeWitness (SNat64 Word64
n)) = SNat n -> IsPrime n
forall (n :: Nat). SNat n -> IsPrime n
PrimeWitness (Integer -> SNat n
forall (n :: Nat). Integer -> SNat n
SNat (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n))

smallPrimeIsSmall :: IsSmallPrime n -> Fits31Bits n
smallPrimeIsSmall :: IsSmallPrime n -> Fits31Bits n
smallPrimeIsSmall (SmallPrimeWitness SNat64 n
sn) = SNat64 n -> Fits31Bits n
forall (n :: Nat). SNat64 n -> Fits31Bits n
Witness31 SNat64 n
sn

-- | Creating small primes
mkSmallPrime :: IsPrime p -> Fits31Bits p -> IsSmallPrime p
mkSmallPrime :: IsPrime p -> Fits31Bits p -> IsSmallPrime p
mkSmallPrime IsPrime p
_ (Witness31 SNat64 p
sn) = SNat64 p -> IsSmallPrime p
forall (n :: Nat). SNat64 n -> IsSmallPrime n
SmallPrimeWitness SNat64 p
sn

-- | Escape hatch
believeMeItsASmallPrime :: SNat64 n -> IsSmallPrime n
believeMeItsASmallPrime :: SNat64 n -> IsSmallPrime n
believeMeItsASmallPrime SNat64 n
sn = SNat64 n -> IsSmallPrime n
forall (n :: Nat). SNat64 n -> IsSmallPrime n
SmallPrimeWitness SNat64 n
sn

--------------------------------------------------------------------------------
-- * Proxy

proxyOf :: a -> Proxy a
proxyOf :: a -> Proxy a
proxyOf a
_ = Proxy a
forall k (t :: k). Proxy t
Proxy

proxyOf1 :: f a -> Proxy a
proxyOf1 :: f a -> Proxy a
proxyOf1 f a
_ = Proxy a
forall k (t :: k). Proxy t
Proxy

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