{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
module Crypto.Number.Nat
( type IsDivisibleBy8
, type IsAtMost, type IsAtLeast
, isDivisibleBy8
, isAtMost
, isAtLeast
) where
import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)
import Crypto.Internal.Nat
isDivisibleBy8 :: KnownNat n => proxy n -> Maybe (IsDiv8 n n :~: 'True)
isDivisibleBy8 :: forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Maybe (IsDiv8 n n :~: 'True)
isDivisibleBy8 proxy n
n
| forall a. Integral a => a -> a -> a
mod (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy n
n) Integer
8 forall a. Eq a => a -> a -> Bool
== Integer
0 = forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl)
| Bool
otherwise = forall a. Maybe a
Nothing
isAtMost :: (KnownNat value, KnownNat bound)
=> proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: 'True)
isAtMost :: forall (value :: Nat) (bound :: Nat) (proxy :: Nat -> *)
(proxy' :: Nat -> *).
(KnownNat value, KnownNat bound) =>
proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: 'True)
isAtMost proxy value
x proxy' bound
y
| forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy value
x forall a. Ord a => a -> a -> Bool
<= forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy' bound
y = forall a. a -> Maybe a
Just (forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl)
| Bool
otherwise = forall a. Maybe a
Nothing
isAtLeast :: (KnownNat value, KnownNat bound)
=> proxy value -> proxy' bound -> Maybe ((bound <=? value) :~: 'True)
isAtLeast :: forall (value :: Nat) (bound :: Nat) (proxy :: Nat -> *)
(proxy' :: Nat -> *).
(KnownNat value, KnownNat bound) =>
proxy value -> proxy' bound -> Maybe ((bound <=? value) :~: 'True)
isAtLeast = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (value :: Nat) (bound :: Nat) (proxy :: Nat -> *)
(proxy' :: Nat -> *).
(KnownNat value, KnownNat bound) =>
proxy value -> proxy' bound -> Maybe ((value <=? bound) :~: 'True)
isAtMost