{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE NoStarIsType #-}
#endif
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
module Closed.Internal where
import Control.DeepSeq
import Control.Monad
import Data.Aeson
import qualified Data.Csv as CSV
import Data.Hashable
import Data.Kind (Type)
import Data.Maybe
import Data.Proxy
import Data.Ratio
import Data.Text (pack)
import Database.Persist.Sql
import GHC.Generics
import GHC.Stack
import GHC.TypeLits
import Test.QuickCheck
newtype Closed (n :: Nat) (m :: Nat)
= Closed { Closed n m -> Integer
getClosed :: Integer }
deriving ((forall x. Closed n m -> Rep (Closed n m) x)
-> (forall x. Rep (Closed n m) x -> Closed n m)
-> Generic (Closed n m)
forall x. Rep (Closed n m) x -> Closed n m
forall x. Closed n m -> Rep (Closed n m) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: Nat) (m :: Nat) x. Rep (Closed n m) x -> Closed n m
forall (n :: Nat) (m :: Nat) x. Closed n m -> Rep (Closed n m) x
$cto :: forall (n :: Nat) (m :: Nat) x. Rep (Closed n m) x -> Closed n m
$cfrom :: forall (n :: Nat) (m :: Nat) x. Closed n m -> Rep (Closed n m) x
Generic)
data Endpoint
= Inclusive Nat
| Exclusive Nat
type family Bounds (lhs :: Endpoint) (rhs :: Endpoint) :: Type where
Bounds (Inclusive n) (Inclusive m) = Closed n m
Bounds (Inclusive n) (Exclusive m) = Closed n (m - 1)
Bounds (Exclusive n) (Inclusive m) = Closed (n + 1) m
Bounds (Exclusive n) (Exclusive m) = Closed (n + 1) (m - 1)
type Single (n :: Nat) = Bounds ('Inclusive n) ('Inclusive n)
type FiniteNat (rhs :: Endpoint) = Bounds ('Inclusive 0) rhs
lowerBound :: Closed n m -> Proxy n
lowerBound :: Closed n m -> Proxy n
lowerBound Closed n m
_ = Proxy n
forall k (t :: k). Proxy t
Proxy
upperBound :: Closed n m -> Proxy m
upperBound :: Closed n m -> Proxy m
upperBound Closed n m
_ = Proxy m
forall k (t :: k). Proxy t
Proxy
closed :: forall n m. (n <= m, KnownNat n, KnownNat m) => Integer -> Maybe (Closed n m)
closed :: Integer -> Maybe (Closed n m)
closed Integer
x = Maybe (Closed n m)
result
where
extracted :: Closed n m
extracted = Maybe (Closed n m) -> Closed n m
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Closed n m)
result
result :: Maybe (Closed n m)
result = do
Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n m -> Proxy n
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy n
lowerBound Closed n m
extracted) Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n m -> Proxy m
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy m
upperBound Closed n m
extracted)
Closed n m -> Maybe (Closed n m)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Closed n m -> Maybe (Closed n m))
-> Closed n m -> Maybe (Closed n m)
forall a b. (a -> b) -> a -> b
$ Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed Integer
x
unsafeClosed :: forall n m. (HasCallStack, n <= m, KnownNat n, KnownNat m) => Integer -> Closed n m
unsafeClosed :: Integer -> Closed n m
unsafeClosed Integer
x = Closed n m
result
where
result :: Closed n m
result =
if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n m -> Proxy n
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy n
lowerBound Closed n m
result) Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n m -> Proxy m
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy m
upperBound Closed n m
result)
then Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed Integer
x
else [Char] -> Closed n m
forall a. HasCallStack => [Char] -> a
error ([Char] -> Closed n m) -> [Char] -> Closed n m
forall a b. (a -> b) -> a -> b
$ Integer -> Closed n m -> [Char] -> [Char]
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Integer -> Closed n m -> [Char] -> [Char]
unrepresentable Integer
x Closed n m
result [Char]
"unsafeClosed"
clamp :: forall n m a. (KnownNat n, KnownNat m, n <= m, Integral a) => a -> Closed n m
clamp :: a -> Closed n m
clamp a
x
| a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Closed n m -> Integer
forall (n :: Nat) (m :: Nat). Closed n m -> Integer
getClosed (Bounded (Closed n m) => Closed n m
forall a. Bounded a => a
minBound @(Closed n m)) = Closed n m
forall a. Bounded a => a
minBound
| a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Closed n m -> Integer
forall (n :: Nat) (m :: Nat). Closed n m -> Integer
getClosed (Bounded (Closed n m) => Closed n m
forall a. Bounded a => a
maxBound @(Closed n m)) = Closed n m
forall a. Bounded a => a
maxBound
| Bool
otherwise = Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
x)
instance Eq (Closed n m) where
Closed Integer
x == :: Closed n m -> Closed n m -> Bool
== Closed Integer
y = Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y
instance Ord (Closed n m) where
Closed Integer
x compare :: Closed n m -> Closed n m -> Ordering
`compare` Closed Integer
y = Integer
x Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Integer
y
instance (n <= m, KnownNat n, KnownNat m) => Bounded (Closed n m) where
maxBound :: Closed n m
maxBound = Closed n m
forall (n :: Nat). Closed n m
result
where
result :: Closed n m
result = Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n m -> Proxy m
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy m
upperBound Closed n m
result))
minBound :: Closed n m
minBound = Closed n m
forall (m :: Nat). Closed n m
result
where
result :: Closed n m
result = Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n m -> Proxy n
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy n
lowerBound Closed n m
result))
instance (n <= m, KnownNat n, KnownNat m) => Enum (Closed n m) where
fromEnum :: Closed n m -> Int
fromEnum = Integer -> Int
forall a. Enum a => a -> Int
fromEnum (Integer -> Int) -> (Closed n m -> Integer) -> Closed n m -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closed n m -> Integer
forall (n :: Nat) (m :: Nat). Closed n m -> Integer
getClosed
toEnum :: Int -> Closed n m
toEnum = Integer -> Closed n m
forall (n :: Nat) (m :: Nat).
(HasCallStack, n <= m, KnownNat n, KnownNat m) =>
Integer -> Closed n m
unsafeClosed (Integer -> Closed n m) -> (Int -> Integer) -> Int -> Closed n m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Enum a => Int -> a
toEnum
enumFrom :: Closed n m -> [Closed n m]
enumFrom Closed n m
x = Closed n m -> Closed n m -> [Closed n m]
forall a. Enum a => a -> a -> [a]
enumFromTo Closed n m
x Closed n m
forall a. Bounded a => a
maxBound
enumFromThen :: Closed n m -> Closed n m -> [Closed n m]
enumFromThen Closed n m
x Closed n m
y = Closed n m -> Closed n m -> Closed n m -> [Closed n m]
forall a. Enum a => a -> a -> a -> [a]
enumFromThenTo Closed n m
x Closed n m
y (if Closed n m
x Closed n m -> Closed n m -> Bool
forall a. Ord a => a -> a -> Bool
>= Closed n m
y then Closed n m
forall a. Bounded a => a
minBound else Closed n m
forall a. Bounded a => a
maxBound)
instance Show (Closed n m) where
showsPrec :: Int -> Closed n m -> [Char] -> [Char]
showsPrec Int
d (Closed Integer
x) = Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (([Char] -> [Char]) -> [Char] -> [Char])
-> ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char]
showString [Char]
"unsafeClosed " ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
10 Integer
x
instance (n <= m, KnownNat n, KnownNat m) => Num (Closed n m) where
Closed Integer
x + :: Closed n m -> Closed n m -> Closed n m
+ Closed Integer
y = Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed n m) -> Integer -> Closed n m
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) (Closed n m -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Closed n m
forall a. Bounded a => a
maxBound :: Closed n m))
Closed Integer
x - :: Closed n m -> Closed n m -> Closed n m
- Closed Integer
y = Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed n m) -> Integer -> Closed n m
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y) (Closed n m -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Closed n m
forall a. Bounded a => a
minBound :: Closed n m))
Closed Integer
x * :: Closed n m -> Closed n m -> Closed n m
* Closed Integer
y = Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed n m) -> Integer -> Closed n m
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) (Closed n m -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Closed n m
forall a. Bounded a => a
maxBound :: Closed n m))
abs :: Closed n m -> Closed n m
abs = Closed n m -> Closed n m
forall a. a -> a
id
signum :: Closed n m -> Closed n m
signum = Closed n m -> Closed n m -> Closed n m
forall a b. a -> b -> a
const Closed n m
1
fromInteger :: Integer -> Closed n m
fromInteger Integer
x = Closed n m
result
where
result :: Closed n m
result =
if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n m -> Proxy n
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy n
lowerBound Closed n m
result) Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n m -> Proxy m
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy m
upperBound Closed n m
result)
then Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed Integer
x
else [Char] -> Closed n m
forall a. HasCallStack => [Char] -> a
error ([Char] -> Closed n m) -> [Char] -> Closed n m
forall a b. (a -> b) -> a -> b
$ Integer -> Closed n m -> [Char] -> [Char]
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Integer -> Closed n m -> [Char] -> [Char]
unrepresentable Integer
x Closed n m
result [Char]
"fromInteger"
instance (n <= m, KnownNat n, KnownNat m) => Real (Closed n m) where
toRational :: Closed n m -> Rational
toRational (Closed Integer
x) = Integer
x Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1
instance (n <= m, KnownNat n, KnownNat m) => Integral (Closed n m) where
quotRem :: Closed n m -> Closed n m -> (Closed n m, Closed n m)
quotRem (Closed Integer
x) (Closed Integer
y) = (Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed n m) -> Integer -> Closed n m
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y, Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed n m) -> Integer -> Closed n m
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
y)
toInteger :: Closed n m -> Integer
toInteger (Closed Integer
x) = Integer
x
instance NFData (Closed n m)
instance Hashable (Closed n m)
instance ToJSON (Closed n m) where
toEncoding :: Closed n m -> Encoding
toEncoding = Integer -> Encoding
forall a. ToJSON a => a -> Encoding
toEncoding (Integer -> Encoding)
-> (Closed n m -> Integer) -> Closed n m -> Encoding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closed n m -> Integer
forall (n :: Nat) (m :: Nat). Closed n m -> Integer
getClosed
toJSON :: Closed n m -> Value
toJSON = Integer -> Value
forall a. ToJSON a => a -> Value
toJSON (Integer -> Value)
-> (Closed n m -> Integer) -> Closed n m -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closed n m -> Integer
forall (n :: Nat) (m :: Nat). Closed n m -> Integer
getClosed
instance (n <= m, KnownNat n, KnownNat m) => FromJSON (Closed n m) where
parseJSON :: Value -> Parser (Closed n m)
parseJSON Value
v = do
Integer
x <- Value -> Parser Integer
forall a. FromJSON a => Value -> Parser a
parseJSON Value
v
case Integer -> Maybe (Closed n m)
forall (n :: Nat) (m :: Nat).
(n <= m, KnownNat n, KnownNat m) =>
Integer -> Maybe (Closed n m)
closed Integer
x of
Just Closed n m
cx -> Closed n m -> Parser (Closed n m)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Closed n m
cx
Maybe (Closed n m)
n -> [Char] -> Parser (Closed n m)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser (Closed n m)) -> [Char] -> Parser (Closed n m)
forall a b. (a -> b) -> a -> b
$ Integer -> Closed n m -> [Char] -> [Char]
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Integer -> Closed n m -> [Char] -> [Char]
unrepresentable Integer
x (Maybe (Closed n m) -> Closed n m
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Closed n m)
n) [Char]
"parseJSON"
instance CSV.ToField (Closed n m) where
toField :: Closed n m -> Field
toField = Integer -> Field
forall a. ToField a => a -> Field
CSV.toField (Integer -> Field)
-> (Closed n m -> Integer) -> Closed n m -> Field
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closed n m -> Integer
forall (n :: Nat) (m :: Nat). Closed n m -> Integer
getClosed
instance (n <= m, KnownNat n, KnownNat m) => CSV.FromField (Closed n m) where
parseField :: Field -> Parser (Closed n m)
parseField Field
s = do
Integer
x <- Field -> Parser Integer
forall a. FromField a => Field -> Parser a
CSV.parseField Field
s
case Integer -> Maybe (Closed n m)
forall (n :: Nat) (m :: Nat).
(n <= m, KnownNat n, KnownNat m) =>
Integer -> Maybe (Closed n m)
closed Integer
x of
Just Closed n m
cx -> Closed n m -> Parser (Closed n m)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Closed n m
cx
Maybe (Closed n m)
n -> [Char] -> Parser (Closed n m)
forall (m :: Type -> Type) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser (Closed n m)) -> [Char] -> Parser (Closed n m)
forall a b. (a -> b) -> a -> b
$ Integer -> Closed n m -> [Char] -> [Char]
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Integer -> Closed n m -> [Char] -> [Char]
unrepresentable Integer
x (Maybe (Closed n m) -> Closed n m
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Closed n m)
n) [Char]
"parseField"
instance (n <= m, KnownNat n, KnownNat m) => Arbitrary (Closed n m) where
arbitrary :: Gen (Closed n m)
arbitrary =
Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed n m) -> Gen Integer -> Gen (Closed n m)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal @n Proxy n
forall k (t :: k). Proxy t
Proxy, Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal @m Proxy m
forall k (t :: k). Proxy t
Proxy)
instance (n <= m, KnownNat n, KnownNat m) => PersistField (Closed n m) where
toPersistValue :: Closed n m -> PersistValue
toPersistValue = Int -> PersistValue
forall a. PersistField a => a -> PersistValue
toPersistValue (Int -> PersistValue)
-> (Closed n m -> Int) -> Closed n m -> PersistValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Integral Integer, Num Int) => Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral @Integer @Int (Integer -> Int) -> (Closed n m -> Integer) -> Closed n m -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closed n m -> Integer
forall (n :: Nat) (m :: Nat). Closed n m -> Integer
getClosed
fromPersistValue :: PersistValue -> Either Text (Closed n m)
fromPersistValue PersistValue
value = do
Integer
x <- (Integral Int, Num Integer) => Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral @Int @Integer (Int -> Integer) -> Either Text Int -> Either Text Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> PersistValue -> Either Text Int
forall a. PersistField a => PersistValue -> Either Text a
fromPersistValue PersistValue
value
case Integer -> Maybe (Closed n m)
forall (n :: Nat) (m :: Nat).
(n <= m, KnownNat n, KnownNat m) =>
Integer -> Maybe (Closed n m)
closed @n @m Integer
x of
Just Closed n m
cx -> Closed n m -> Either Text (Closed n m)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Closed n m
cx
Maybe (Closed n m)
n -> Text -> Either Text (Closed n m)
forall a b. a -> Either a b
Left (Text -> Either Text (Closed n m))
-> Text -> Either Text (Closed n m)
forall a b. (a -> b) -> a -> b
$ [Char] -> Text
pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ Integer -> Closed n m -> [Char] -> [Char]
forall (n :: Nat) (m :: Nat).
(KnownNat n, KnownNat m) =>
Integer -> Closed n m -> [Char] -> [Char]
unrepresentable Integer
x (Maybe (Closed n m) -> Closed n m
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Closed n m)
n) [Char]
"fromPersistValue"
instance (n <= m, KnownNat n, KnownNat m) => PersistFieldSql (Closed n m) where
sqlType :: Proxy (Closed n m) -> SqlType
sqlType Proxy (Closed n m)
_ = Proxy Int -> SqlType
forall a. PersistFieldSql a => Proxy a -> SqlType
sqlType (Proxy Int
forall k (t :: k). Proxy t
Proxy @Int)
unrepresentable :: (KnownNat n, KnownNat m) => Integer -> Closed n m -> String -> String
unrepresentable :: Integer -> Closed n m -> [Char] -> [Char]
unrepresentable Integer
x Closed n m
cx [Char]
prefix =
[Char]
prefix [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": Integer " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
" is not representable in Closed " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n -> Integer) -> Proxy n -> Integer
forall a b. (a -> b) -> a -> b
$ Closed n m -> Proxy n
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy n
lowerBound Closed n m
cx) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy m -> Integer) -> Proxy m -> Integer
forall a b. (a -> b) -> a -> b
$ Closed n m -> Proxy m
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy m
upperBound Closed n m
cx)
natToClosed :: forall n m x proxy. (n <= x, x <= m, KnownNat x, KnownNat n, KnownNat m) => proxy x -> Closed n m
natToClosed :: proxy x -> Closed n m
natToClosed proxy x
p = Integer -> Closed n m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed n m) -> Integer -> Closed n m
forall a b. (a -> b) -> a -> b
$ proxy x -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal proxy x
p
weakenUpper :: forall k n m. (n <= m, m <= k) => Closed n m -> Closed n k
weakenUpper :: Closed n m -> Closed n k
weakenUpper (Closed Integer
x) = Integer -> Closed n k
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed Integer
x
weakenLower :: forall k n m. (n <= m, k <= n) => Closed n m -> Closed k m
weakenLower :: Closed n m -> Closed k m
weakenLower (Closed Integer
x) = Integer -> Closed k m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed Integer
x
strengthenUpper :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed n k)
strengthenUpper :: Closed n m -> Maybe (Closed n k)
strengthenUpper (Closed Integer
x) = Maybe (Closed n k)
result
where
result :: Maybe (Closed n k)
result = do
Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Proxy k -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n k -> Proxy k
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy m
upperBound (Closed n k -> Proxy k) -> Closed n k -> Proxy k
forall a b. (a -> b) -> a -> b
$ Maybe (Closed n k) -> Closed n k
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Closed n k)
result)
Closed n k -> Maybe (Closed n k)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Closed n k -> Maybe (Closed n k))
-> Closed n k -> Maybe (Closed n k)
forall a b. (a -> b) -> a -> b
$ Integer -> Closed n k
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed Integer
x
strengthenLower :: forall k n m. (KnownNat n, KnownNat m, KnownNat k, n <= m, n <= k, k <= m) => Closed n m -> Maybe (Closed k m)
strengthenLower :: Closed n m -> Maybe (Closed k m)
strengthenLower (Closed Integer
x) = Maybe (Closed k m)
result
where
result :: Maybe (Closed k m)
result = do
Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Proxy k -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed k m -> Proxy k
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy n
lowerBound (Closed k m -> Proxy k) -> Closed k m -> Proxy k
forall a b. (a -> b) -> a -> b
$ Maybe (Closed k m) -> Closed k m
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (Closed k m)
result)
Closed k m -> Maybe (Closed k m)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Closed k m -> Maybe (Closed k m))
-> Closed k m -> Maybe (Closed k m)
forall a b. (a -> b) -> a -> b
$ Integer -> Closed k m
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed Integer
x
equals :: Closed n m -> Closed o p -> Bool
equals :: Closed n m -> Closed o p -> Bool
equals (Closed Integer
x) (Closed Integer
y) = Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
y
infix 4 `equals`
cmp :: Closed n m -> Closed o p -> Ordering
cmp :: Closed n m -> Closed o p -> Ordering
cmp (Closed Integer
x) (Closed Integer
y) = Integer
x Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Integer
y
add :: Closed n m -> Closed o p -> Closed (n + o) (m + p)
add :: Closed n m -> Closed o p -> Closed (n + o) (m + p)
add (Closed Integer
x) (Closed Integer
y) = Integer -> Closed (n + o) (m + p)
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed (n + o) (m + p))
-> Integer -> Closed (n + o) (m + p)
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y
sub :: Closed n m -> Closed o p -> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
sub :: Closed n m
-> Closed o p
-> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
sub (Closed Integer
x) (Closed Integer
y)
| Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
y = Closed (n - o) (m - p)
-> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
forall a b. b -> Either a b
Right (Closed (n - o) (m - p)
-> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p)))
-> Closed (n - o) (m - p)
-> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
forall a b. (a -> b) -> a -> b
$ Integer -> Closed (n - o) (m - p)
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed (n - o) (m - p))
-> Integer -> Closed (n - o) (m - p)
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y
| Bool
otherwise = Closed (o - n) (p - m)
-> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
forall a b. a -> Either a b
Left (Closed (o - n) (p - m)
-> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p)))
-> Closed (o - n) (p - m)
-> Either (Closed (o - n) (p - m)) (Closed (n - o) (m - p))
forall a b. (a -> b) -> a -> b
$ Integer -> Closed (o - n) (p - m)
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed (o - n) (p - m))
-> Integer -> Closed (o - n) (p - m)
forall a b. (a -> b) -> a -> b
$ Integer
y Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
x
multiply :: Closed n m -> Closed o p -> Closed (n * o) (m * p)
multiply :: Closed n m -> Closed o p -> Closed (n * o) (m * p)
multiply (Closed Integer
x) (Closed Integer
y) = Integer -> Closed (n * o) (m * p)
forall (n :: Nat) (m :: Nat). Integer -> Closed n m
Closed (Integer -> Closed (n * o) (m * p))
-> Integer -> Closed (n * o) (m * p)
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y
isValidClosed :: (KnownNat n, KnownNat m) => Closed n m -> Bool
isValidClosed :: Closed n m -> Bool
isValidClosed cx :: Closed n m
cx@(Closed Integer
x) =
Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n m -> Proxy n
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy n
lowerBound Closed n m
cx) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Proxy m -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Closed n m -> Proxy m
forall (n :: Nat) (m :: Nat). Closed n m -> Proxy m
upperBound Closed n m
cx)