{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- Prevent kind errors arising from using * to mean multiplication on
-- type-level natural numbers.
#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)

-- | Describe whether the endpoint of a 'Bounds' includes
-- or excludes its argument
data Endpoint
  -- | Endpoint includes its argument
  = Inclusive Nat
  -- | Endpoint excludes its argument
  | Exclusive Nat

-- | Syntactic sugar to express open and half-open intervals using
-- the 'Closed' type
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)

-- | Syntactic sugar to express a value that has only one non-bottom
-- inhabitant using the 'Closed' type
type Single (n :: Nat) = Bounds ('Inclusive n) ('Inclusive n)

-- | Syntactic sugar to express a value whose lower bound is zero
type FiniteNat (rhs :: Endpoint) = Bounds ('Inclusive 0) rhs

-- | Proxy for the lower bound of a 'Closed' value
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

-- | Proxy for the upper bound of a 'Closed' value
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

-- | Safely create a 'Closed' value using the specified argument
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

-- | Create a 'Closed' value throwing an error if the argument is not in range
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 an @'Integral'@ in the range constrained by a @'Closed'@ interval
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)

-- | Test equality on 'Closed' values in the same range
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

-- | Compare 'Closed' values in the same range
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

-- | Generate the lowest and highest inhabitant of a given 'Closed' type
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))

-- | Enumerate values in the range of a given 'Closed' type
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

-- | Bounded arithmetic, e.g. maxBound + 1 == maxBound
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)

-- | Convert a type-level literal into a 'Closed' value
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

-- | Add inhabitants at the end
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

-- | Add inhabitants at the beginning
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

-- | Remove inhabitants from the end. Returns 'Nothing' if the input was removed
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

-- | Remove inhabitants from the beginning. Returns 'Nothing' if the input was removed
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

-- | Test two different types of 'Closed' values for equality.
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`

-- | Compare two different types of 'Closed' values
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 two different types of 'Closed' values
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

-- | Subtract two different types of 'Closed' values
-- Returns 'Left' for negative results, and 'Right' for positive results.
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 two different types of 'Closed' values
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

-- | Verifies that a given 'Closed' value is valid.
-- Should always return 'True' unles you bring the @Closed.Internal.Closed@ constructor into scope,
-- or use 'Unsafe.Coerce.unsafeCoerce' or other nasty hacks
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)