{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoImplicitPrelude #-}

{-# OPTIONS -Wno-unticked-promoted-constructors #-}

-- | See 'Measure'
module Data.Measure.Class (
  BoundedMeasure (..),
  Measure (..),

  -- * Exceptions
  DataMeasureClassOverflowException (..),
)
where

import Control.Exception (Exception, throw)
import Data.Coerce
import Data.DerivingVia
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Generics
#if __GLASGOW_HASKELL__ < 900
-- Use the GHC version here because this is compiler dependent, and only indirectly lib dependent.
import GHC.Natural (Natural)
#endif
import GHC.TypeLits
import Prelude (($))
import qualified Prelude

-- | Core combinators for a possibly-multidimensional measurement
--
-- @a@ is a fixed set of measurements of a /single/ object. It is not the
-- measurements from multiple objects.
--
-- - @('zero', 'plus')@ is a commutative monoid
--
-- - @('zero', 'max')@ is a bounded join-semilattice
--
-- - @('min', 'max')@ is a lattice
--
-- - /lattice-ordered monoid/ @'min' ('plus' a b) ('plus' a c) = a + 'min' b c@
--
-- Note that the bounded join-semilattice precludes negative (components of)
-- measurements.
class Prelude.Eq a => Measure a where
  -- | The measurement of nothing
  --
  -- See 'Measure' for laws.
  zero :: a

  -- | Combine two measurements
  --
  -- If @a@ consists of multiple measurements, this is componentwise.
  --
  -- See 'Measure' for laws.
  plus :: a -> a -> a

  -- | The lesser of two measurements
  --
  -- If @a@ consists of multiple measurements, this is componentwise.
  --
  -- See 'Measure' for laws.
  min :: a -> a -> a

  -- | The greater of two measurements
  --
  -- If @a@ consists of multiple measurements, this is componentwise.
  --
  -- See 'Measure' for laws.
  max :: a -> a -> a

-- | A unique maximal measurement
--
-- - @('maxBound', 'min')@ is a bounded meet-semilattice
class Measure a => BoundedMeasure a where
  -- | A unique maximal measurement
  --
  -- See 'BoundedMeasure' for laws.
  maxBound :: a

--------------------------------------------------------------------------------
-- Primitive instances
--------------------------------------------------------------------------------

-- we conservatively don't instantiate for types that represent negative
-- numbers

instance Measure Natural where
  zero :: Natural
zero = Natural
0
  plus :: Natural -> Natural -> Natural
plus = forall a. Num a => a -> a -> a
(Prelude.+)
  min :: Natural -> Natural -> Natural
min = forall a. Ord a => a -> a -> a
Prelude.min
  max :: Natural -> Natural -> Natural
max = forall a. Ord a => a -> a -> a
Prelude.max

deriving via
  InstantiatedAt Generic (a, b)
  instance
    (Measure a, Measure b) => Measure (a, b)

deriving via
  InstantiatedAt Generic (a, b, c)
  instance
    (Measure a, Measure b, Measure c) => Measure (a, b, c)

deriving via
  InstantiatedAt Generic (a, b, c, d)
  instance
    (Measure a, Measure b, Measure c, Measure d) =>
    Measure (a, b, c, d)

deriving via
  InstantiatedAt Generic (a, b, c, d, e)
  instance
    (Measure a, Measure b, Measure c, Measure d, Measure e) =>
    Measure (a, b, c, d, e)

deriving via
  InstantiatedAt Generic (a, b, c, d, e, f)
  instance
    (Measure a, Measure b, Measure c, Measure d, Measure e, Measure f) =>
    Measure (a, b, c, d, e, f)

deriving via
  InstantiatedAt Generic (a, b, c, d, e, f, g)
  instance
    ( Measure a
    , Measure b
    , Measure c
    , Measure d
    , Measure e
    , Measure f
    , Measure g
    ) =>
    Measure (a, b, c, d, e, f, g)

-- larger tuples unfortunatley do not have Generic instances

-- | 'plus' throws 'DataMeasureClassOverflowException'
instance Measure Word8 where
  zero :: Word8
zero = Word8
0
  plus :: Word8 -> Word8 -> Word8
plus = forall a. (Bounded a, Integral a) => a -> a -> a
checkedPlus
  min :: Word8 -> Word8 -> Word8
min = forall a. Ord a => a -> a -> a
Prelude.min
  max :: Word8 -> Word8 -> Word8
max = forall a. Ord a => a -> a -> a
Prelude.max

instance BoundedMeasure Word8 where
  maxBound :: Word8
maxBound = forall a. Bounded a => a
Prelude.maxBound

-- | 'plus' throws 'DataMeasureClassOverflowException'
instance Measure Word16 where
  zero :: Word16
zero = Word16
0
  plus :: Word16 -> Word16 -> Word16
plus = forall a. (Bounded a, Integral a) => a -> a -> a
checkedPlus
  min :: Word16 -> Word16 -> Word16
min = forall a. Ord a => a -> a -> a
Prelude.min
  max :: Word16 -> Word16 -> Word16
max = forall a. Ord a => a -> a -> a
Prelude.max

instance BoundedMeasure Word16 where
  maxBound :: Word16
maxBound = forall a. Bounded a => a
Prelude.maxBound

-- | 'plus' throws 'DataMeasureClassOverflowException'
instance Measure Word32 where
  zero :: Word32
zero = Word32
0
  plus :: Word32 -> Word32 -> Word32
plus = forall a. (Bounded a, Integral a) => a -> a -> a
checkedPlus
  min :: Word32 -> Word32 -> Word32
min = forall a. Ord a => a -> a -> a
Prelude.min
  max :: Word32 -> Word32 -> Word32
max = forall a. Ord a => a -> a -> a
Prelude.max

instance BoundedMeasure Word32 where
  maxBound :: Word32
maxBound = forall a. Bounded a => a
Prelude.maxBound

-- | 'plus' throws 'DataMeasureClassOverflowException'
instance Measure Word64 where
  zero :: Word64
zero = Word64
0
  plus :: Word64 -> Word64 -> Word64
plus = forall a. (Bounded a, Integral a) => a -> a -> a
checkedPlus
  min :: Word64 -> Word64 -> Word64
min = forall a. Ord a => a -> a -> a
Prelude.min
  max :: Word64 -> Word64 -> Word64
max = forall a. Ord a => a -> a -> a
Prelude.max

instance BoundedMeasure Word64 where
  maxBound :: Word64
maxBound = forall a. Bounded a => a
Prelude.maxBound

-- not exported
--
-- Throws 'DataMeasureClassOverflowException'
checkedPlus ::
  (Prelude.Bounded a, Prelude.Integral a) =>
  a -> a -> a
checkedPlus :: forall a. (Bounded a, Integral a) => a -> a -> a
checkedPlus a
x a
y =
  if a
x forall a. Ord a => a -> a -> Bool
Prelude.> forall a. Bounded a => a
Prelude.maxBound forall a. Num a => a -> a -> a
Prelude.- a
y
    then forall a e. Exception e => e -> a
throw DataMeasureClassOverflowException
DataMeasureClassOverflowException
    else a
x forall a. Num a => a -> a -> a
Prelude.+ a
y

-- | An exception thrown by 'plus' on overflow, since overflow violates
-- /lattice-ordered monoid/
data DataMeasureClassOverflowException = DataMeasureClassOverflowException
  deriving (Int -> DataMeasureClassOverflowException -> ShowS
[DataMeasureClassOverflowException] -> ShowS
DataMeasureClassOverflowException -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataMeasureClassOverflowException] -> ShowS
$cshowList :: [DataMeasureClassOverflowException] -> ShowS
show :: DataMeasureClassOverflowException -> String
$cshow :: DataMeasureClassOverflowException -> String
showsPrec :: Int -> DataMeasureClassOverflowException -> ShowS
$cshowsPrec :: Int -> DataMeasureClassOverflowException -> ShowS
Prelude.Show)

instance Exception DataMeasureClassOverflowException

--------------------------------------------------------------------------------
-- DerivingVia instances via these classes
--------------------------------------------------------------------------------

-- | The @('zero', 'plus')@ monoid
instance Measure a => Prelude.Monoid (InstantiatedAt Measure a) where
  mempty :: InstantiatedAt Measure a
mempty = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Measure a => a
zero @a

-- | The @('zero', 'plus')@ monoid
instance Measure a => Prelude.Semigroup (InstantiatedAt Measure a) where
  <> :: InstantiatedAt Measure a
-> InstantiatedAt Measure a -> InstantiatedAt Measure a
(<>) = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Measure a => a -> a -> a
plus @a

--------------------------------------------------------------------------------
-- DerivingVia instances of these classes
--------------------------------------------------------------------------------

instance
  (Prelude.Monoid a, Prelude.Ord a) =>
  Measure (InstantiatedAt Prelude.Ord a)
  where
  zero :: InstantiatedAt Ord a
zero = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a
Prelude.mempty @a
  plus :: InstantiatedAt Ord a
-> InstantiatedAt Ord a -> InstantiatedAt Ord a
plus = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Semigroup a => a -> a -> a
(Prelude.<>) @a
  min :: InstantiatedAt Ord a
-> InstantiatedAt Ord a -> InstantiatedAt Ord a
min = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
Prelude.min @a
  max :: InstantiatedAt Ord a
-> InstantiatedAt Ord a -> InstantiatedAt Ord a
max = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
Prelude.max @a

instance
  (Prelude.Bounded a, Prelude.Monoid a, Prelude.Ord a) =>
  BoundedMeasure (InstantiatedAt Prelude.Ord a)
  where
  maxBound :: InstantiatedAt Ord a
maxBound = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Bounded a => a
Prelude.maxBound @a

instance
  (Prelude.Eq a, Generic a, GMeasure (Rep a)) =>
  Measure (InstantiatedAt Generic a)
  where
  zero :: InstantiatedAt Generic a
zero = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a x. Generic a => Rep a x -> a
to @a forall (rep :: * -> *) x. GMeasure rep => rep x
gzero
  plus :: InstantiatedAt Generic a
-> InstantiatedAt Generic a -> InstantiatedAt Generic a
plus = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a.
Generic a =>
(forall x. Rep a x -> Rep a x -> Rep a x) -> a -> a -> a
gbinop @a forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gplus
  min :: InstantiatedAt Generic a
-> InstantiatedAt Generic a -> InstantiatedAt Generic a
min = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a.
Generic a =>
(forall x. Rep a x -> Rep a x -> Rep a x) -> a -> a -> a
gbinop @a forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmin
  max :: InstantiatedAt Generic a
-> InstantiatedAt Generic a -> InstantiatedAt Generic a
max = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a.
Generic a =>
(forall x. Rep a x -> Rep a x -> Rep a x) -> a -> a -> a
gbinop @a forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmax

instance
  (Prelude.Eq a, Generic a, GBoundedMeasure (Rep a), GMeasure (Rep a)) =>
  BoundedMeasure (InstantiatedAt Generic a)
  where
  maxBound :: InstantiatedAt Generic a
maxBound = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a x. Generic a => Rep a x -> a
to @a forall (rep :: * -> *) x. GBoundedMeasure rep => rep x
gmaxBound

-- not exported
gbinop ::
  Generic a => (forall x. Rep a x -> Rep a x -> Rep a x) -> a -> a -> a
gbinop :: forall a.
Generic a =>
(forall x. Rep a x -> Rep a x -> Rep a x) -> a -> a -> a
gbinop forall x. Rep a x -> Rep a x -> Rep a x
f a
l a
r = forall a x. Generic a => Rep a x -> a
to forall a b. (a -> b) -> a -> b
$ forall x. Rep a x -> Rep a x -> Rep a x
f (forall a x. Generic a => a -> Rep a x
from a
l) (forall a x. Generic a => a -> Rep a x
from a
r)

class GMeasure rep where
  gzero :: rep x
  gplus :: rep x -> rep x -> rep x
  gmin :: rep x -> rep x -> rep x
  gmax :: rep x -> rep x -> rep x

instance Measure c => GMeasure (K1 i c) where
  gzero :: forall x. K1 i c x
gzero = forall k i c (p :: k). c -> K1 i c p
K1 forall a. Measure a => a
zero
  gplus :: forall x. K1 i c x -> K1 i c x -> K1 i c x
gplus (K1 c
l) (K1 c
r) = forall k i c (p :: k). c -> K1 i c p
K1 (forall a. Measure a => a -> a -> a
plus c
l c
r)
  gmin :: forall x. K1 i c x -> K1 i c x -> K1 i c x
gmin (K1 c
l) (K1 c
r) = forall k i c (p :: k). c -> K1 i c p
K1 (forall a. Measure a => a -> a -> a
min c
l c
r)
  gmax :: forall x. K1 i c x -> K1 i c x -> K1 i c x
gmax (K1 c
l) (K1 c
r) = forall k i c (p :: k). c -> K1 i c p
K1 (forall a. Measure a => a -> a -> a
max c
l c
r)

instance GMeasure f => GMeasure (M1 i c f) where
  gzero :: forall x. M1 i c f x
gzero = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (rep :: * -> *) x. GMeasure rep => rep x
gzero
  gplus :: forall x. M1 i c f x -> M1 i c f x -> M1 i c f x
gplus (M1 f x
l) (M1 f x
r) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gplus f x
l f x
r)
  gmin :: forall x. M1 i c f x -> M1 i c f x -> M1 i c f x
gmin (M1 f x
l) (M1 f x
r) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmin f x
l f x
r)
  gmax :: forall x. M1 i c f x -> M1 i c f x -> M1 i c f x
gmax (M1 f x
l) (M1 f x
r) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmax f x
l f x
r)

instance GMeasure V1 where
  gzero :: forall x. V1 x
gzero = forall a. HasCallStack => String -> a
Prelude.error String
"GMeasure V1"
  gplus :: forall x. V1 x -> V1 x -> V1 x
gplus = \case {}
  gmin :: forall x. V1 x -> V1 x -> V1 x
gmin = \case {}
  gmax :: forall x. V1 x -> V1 x -> V1 x
gmax = \case {}

instance GMeasure U1 where
  gzero :: forall x. U1 x
gzero = forall k (p :: k). U1 p
U1
  gplus :: forall x. U1 x -> U1 x -> U1 x
gplus U1 x
U1 U1 x
U1 = forall k (p :: k). U1 p
U1
  gmin :: forall x. U1 x -> U1 x -> U1 x
gmin U1 x
U1 U1 x
U1 = forall k (p :: k). U1 p
U1
  gmax :: forall x. U1 x -> U1 x -> U1 x
gmax U1 x
U1 U1 x
U1 = forall k (p :: k). U1 p
U1

instance (GMeasure l, GMeasure r) => GMeasure (l :*: r) where
  gzero :: forall x. (:*:) l r x
gzero = forall (rep :: * -> *) x. GMeasure rep => rep x
gzero forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) x. GMeasure rep => rep x
gzero
  gplus :: forall x. (:*:) l r x -> (:*:) l r x -> (:*:) l r x
gplus (l x
l1 :*: r x
r1) (l x
l2 :*: r x
r2) = forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gplus l x
l1 l x
l2 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gplus r x
r1 r x
r2
  gmin :: forall x. (:*:) l r x -> (:*:) l r x -> (:*:) l r x
gmin (l x
l1 :*: r x
r1) (l x
l2 :*: r x
r2) = forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmin l x
l1 l x
l2 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmin r x
r1 r x
r2
  gmax :: forall x. (:*:) l r x -> (:*:) l r x -> (:*:) l r x
gmax (l x
l1 :*: r x
r1) (l x
l2 :*: r x
r2) = forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmax l x
l1 l x
l2 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmax r x
r1 r x
r2

instance
  TypeError
    ( Text "No Generics definition of "
        :<>: ShowType Measure
        :<>: Text " for types with multiple constructors "
        :<>: ShowType (l :+: r)
    ) =>
  GMeasure (l :+: r)
  where
  gzero :: forall x. (:+:) l r x
gzero = forall a. HasCallStack => String -> a
Prelude.error String
"GMeasure gzero :+:"
  gplus :: forall x. (:+:) l r x -> (:+:) l r x -> (:+:) l r x
gplus = forall a. HasCallStack => String -> a
Prelude.error String
"GMeasure gplus :+:"
  gmin :: forall x. (:+:) l r x -> (:+:) l r x -> (:+:) l r x
gmin = forall a. HasCallStack => String -> a
Prelude.error String
"GMeasure gmin :+:"
  gmax :: forall x. (:+:) l r x -> (:+:) l r x -> (:+:) l r x
gmax = forall a. HasCallStack => String -> a
Prelude.error String
"GMeasure gmax :+:"

class GBoundedMeasure rep where
  gmaxBound :: rep x

instance BoundedMeasure c => GBoundedMeasure (K1 i c) where
  gmaxBound :: forall x. K1 i c x
gmaxBound = forall k i c (p :: k). c -> K1 i c p
K1 forall a. BoundedMeasure a => a
maxBound

instance GBoundedMeasure f => GBoundedMeasure (M1 i c f) where
  gmaxBound :: forall x. M1 i c f x
gmaxBound = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (rep :: * -> *) x. GBoundedMeasure rep => rep x
gmaxBound

instance GBoundedMeasure V1 where
  gmaxBound :: forall x. V1 x
gmaxBound = forall a. HasCallStack => String -> a
Prelude.error String
"GBoundedMeasure V1"

instance GBoundedMeasure U1 where
  gmaxBound :: forall x. U1 x
gmaxBound = forall k (p :: k). U1 p
U1

instance (GBoundedMeasure l, GBoundedMeasure r) => GBoundedMeasure (l :*: r) where
  gmaxBound :: forall x. (:*:) l r x
gmaxBound = forall (rep :: * -> *) x. GBoundedMeasure rep => rep x
gmaxBound forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (rep :: * -> *) x. GBoundedMeasure rep => rep x
gmaxBound

instance
  TypeError
    ( Text "No Generics definition of "
        :<>: ShowType BoundedMeasure
        :<>: Text " for types with multiple constructors "
        :<>: ShowType (l :+: r)
    ) =>
  GBoundedMeasure (l :+: r)
  where
  gmaxBound :: forall x. (:+:) l r x
gmaxBound = forall a. HasCallStack => String -> a
Prelude.error String
"GBoundedMeasure :+:"