{-# 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
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 = Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(Prelude.+)
  min :: Natural -> Natural -> Natural
min = Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
Prelude.min
  max :: Natural -> Natural -> Natural
max = Natural -> Natural -> Natural
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 = Word8 -> Word8 -> Word8
forall a. (Bounded a, Integral a) => a -> a -> a
checkedPlus
  min :: Word8 -> Word8 -> Word8
min = Word8 -> Word8 -> Word8
forall a. Ord a => a -> a -> a
Prelude.min
  max :: Word8 -> Word8 -> Word8
max = Word8 -> Word8 -> Word8
forall a. Ord a => a -> a -> a
Prelude.max

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

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

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

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

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

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

instance BoundedMeasure Word64 where
  maxBound :: Word64
maxBound = Word64
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 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
Prelude.> a
forall a. Bounded a => a
Prelude.maxBound a -> a -> a
forall a. Num a => a -> a -> a
Prelude.- a
y
    then DataMeasureClassOverflowException -> a
forall a e. Exception e => e -> a
throw DataMeasureClassOverflowException
DataMeasureClassOverflowException
    else a
x a -> a -> a
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
(Int -> DataMeasureClassOverflowException -> ShowS)
-> (DataMeasureClassOverflowException -> String)
-> ([DataMeasureClassOverflowException] -> ShowS)
-> Show DataMeasureClassOverflowException
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DataMeasureClassOverflowException -> ShowS
showsPrec :: Int -> DataMeasureClassOverflowException -> ShowS
$cshow :: DataMeasureClassOverflowException -> String
show :: DataMeasureClassOverflowException -> String
$cshowList :: [DataMeasureClassOverflowException] -> ShowS
showList :: [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 = a -> InstantiatedAt Measure a
forall a b. Coercible a b => a -> b
coerce (a -> InstantiatedAt Measure a) -> a -> InstantiatedAt Measure a
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
(<>) = (a -> a -> a)
-> InstantiatedAt Measure a
-> InstantiatedAt Measure a
-> InstantiatedAt Measure a
forall a b. Coercible a b => a -> b
coerce ((a -> a -> a)
 -> InstantiatedAt Measure a
 -> InstantiatedAt Measure a
 -> InstantiatedAt Measure a)
-> (a -> a -> a)
-> InstantiatedAt Measure a
-> InstantiatedAt Measure a
-> InstantiatedAt Measure a
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 = a -> InstantiatedAt Ord a
forall a b. Coercible a b => a -> b
coerce (a -> InstantiatedAt Ord a) -> a -> InstantiatedAt Ord a
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 = (a -> a -> a)
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
forall a b. Coercible a b => a -> b
coerce ((a -> a -> a)
 -> InstantiatedAt Ord a
 -> InstantiatedAt Ord a
 -> InstantiatedAt Ord a)
-> (a -> a -> a)
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
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 = (a -> a -> a)
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
forall a b. Coercible a b => a -> b
coerce ((a -> a -> a)
 -> InstantiatedAt Ord a
 -> InstantiatedAt Ord a
 -> InstantiatedAt Ord a)
-> (a -> a -> a)
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
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 = (a -> a -> a)
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
forall a b. Coercible a b => a -> b
coerce ((a -> a -> a)
 -> InstantiatedAt Ord a
 -> InstantiatedAt Ord a
 -> InstantiatedAt Ord a)
-> (a -> a -> a)
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
-> InstantiatedAt Ord a
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 = a -> InstantiatedAt Ord a
forall a b. Coercible a b => a -> b
coerce (a -> InstantiatedAt Ord a) -> a -> InstantiatedAt Ord a
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 = a -> InstantiatedAt Generic a
forall a b. Coercible a b => a -> b
coerce (a -> InstantiatedAt Generic a) -> a -> InstantiatedAt Generic a
forall a b. (a -> b) -> a -> b
$ forall a x. Generic a => Rep a x -> a
to @a Rep a Any
forall x. Rep a x
forall (rep :: * -> *) x. GMeasure rep => rep x
gzero
  plus :: InstantiatedAt Generic a
-> InstantiatedAt Generic a -> InstantiatedAt Generic a
plus = (a -> a -> a)
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
forall a b. Coercible a b => a -> b
coerce ((a -> a -> a)
 -> InstantiatedAt Generic a
 -> InstantiatedAt Generic a
 -> InstantiatedAt Generic a)
-> (a -> a -> a)
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
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 Rep a x -> Rep a x -> Rep a x
forall x. Rep a x -> Rep a x -> Rep a x
forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gplus
  min :: InstantiatedAt Generic a
-> InstantiatedAt Generic a -> InstantiatedAt Generic a
min = (a -> a -> a)
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
forall a b. Coercible a b => a -> b
coerce ((a -> a -> a)
 -> InstantiatedAt Generic a
 -> InstantiatedAt Generic a
 -> InstantiatedAt Generic a)
-> (a -> a -> a)
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
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 Rep a x -> Rep a x -> Rep a x
forall x. Rep a x -> Rep a x -> Rep a x
forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmin
  max :: InstantiatedAt Generic a
-> InstantiatedAt Generic a -> InstantiatedAt Generic a
max = (a -> a -> a)
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
forall a b. Coercible a b => a -> b
coerce ((a -> a -> a)
 -> InstantiatedAt Generic a
 -> InstantiatedAt Generic a
 -> InstantiatedAt Generic a)
-> (a -> a -> a)
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
-> InstantiatedAt Generic a
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 Rep a x -> Rep a x -> Rep a x
forall x. Rep a x -> Rep a x -> Rep a x
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 = a -> InstantiatedAt Generic a
forall a b. Coercible a b => a -> b
coerce (a -> InstantiatedAt Generic a) -> a -> InstantiatedAt Generic a
forall a b. (a -> b) -> a -> b
$ forall a x. Generic a => Rep a x -> a
to @a Rep a Any
forall x. Rep a x
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 = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> Rep a Any -> a
forall a b. (a -> b) -> a -> b
$ Rep a Any -> Rep a Any -> Rep a Any
forall x. Rep a x -> Rep a x -> Rep a x
f (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
l) (a -> Rep a Any
forall x. a -> Rep a x
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 = c -> K1 i c x
forall k i c (p :: k). c -> K1 i c p
K1 c
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) = c -> K1 i c x
forall k i c (p :: k). c -> K1 i c p
K1 (c -> c -> c
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) = c -> K1 i c x
forall k i c (p :: k). c -> K1 i c p
K1 (c -> c -> c
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) = c -> K1 i c x
forall k i c (p :: k). c -> K1 i c p
K1 (c -> c -> c
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 = f x -> M1 i c f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 f x
forall x. f x
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) = f x -> M1 i c f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f x -> f x -> f x
forall x. f x -> f x -> f x
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) = f x -> M1 i c f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f x -> f x -> f x
forall x. f x -> f x -> f x
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) = f x -> M1 i c f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f x -> f x -> f x
forall x. f x -> f x -> f x
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 = String -> V1 x
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 = U1 x
forall k (p :: k). U1 p
U1
  gplus :: forall x. U1 x -> U1 x -> U1 x
gplus U1 x
U1 U1 x
U1 = U1 x
forall k (p :: k). U1 p
U1
  gmin :: forall x. U1 x -> U1 x -> U1 x
gmin U1 x
U1 U1 x
U1 = U1 x
forall k (p :: k). U1 p
U1
  gmax :: forall x. U1 x -> U1 x -> U1 x
gmax U1 x
U1 U1 x
U1 = U1 x
forall k (p :: k). U1 p
U1

instance (GMeasure l, GMeasure r) => GMeasure (l :*: r) where
  gzero :: forall x. (:*:) l r x
gzero = l x
forall x. l x
forall (rep :: * -> *) x. GMeasure rep => rep x
gzero l x -> r x -> (:*:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: r x
forall x. r x
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) = l x -> l x -> l x
forall x. l x -> l x -> l x
forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gplus l x
l1 l x
l2 l x -> r x -> (:*:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: r x -> r x -> r x
forall x. r x -> r x -> r x
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) = l x -> l x -> l x
forall x. l x -> l x -> l x
forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmin l x
l1 l x
l2 l x -> r x -> (:*:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: r x -> r x -> r x
forall x. r x -> r x -> r x
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) = l x -> l x -> l x
forall x. l x -> l x -> l x
forall (rep :: * -> *) x. GMeasure rep => rep x -> rep x -> rep x
gmax l x
l1 l x
l2 l x -> r x -> (:*:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: r x -> r x -> r x
forall x. r x -> r x -> r x
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 = String -> (:+:) l r x
forall a. HasCallStack => String -> a
Prelude.error String
"GMeasure gzero :+:"
  gplus :: forall x. (:+:) l r x -> (:+:) l r x -> (:+:) l r x
gplus = String -> (:+:) l r x -> (:+:) l r x -> (:+:) l r x
forall a. HasCallStack => String -> a
Prelude.error String
"GMeasure gplus :+:"
  gmin :: forall x. (:+:) l r x -> (:+:) l r x -> (:+:) l r x
gmin = String -> (:+:) l r x -> (:+:) l r x -> (:+:) l r x
forall a. HasCallStack => String -> a
Prelude.error String
"GMeasure gmin :+:"
  gmax :: forall x. (:+:) l r x -> (:+:) l r x -> (:+:) l r x
gmax = String -> (:+:) l r x -> (:+:) l r x -> (:+:) l r x
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 = c -> K1 i c x
forall k i c (p :: k). c -> K1 i c p
K1 c
forall a. BoundedMeasure a => a
maxBound

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

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

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

instance (GBoundedMeasure l, GBoundedMeasure r) => GBoundedMeasure (l :*: r) where
  gmaxBound :: forall x. (:*:) l r x
gmaxBound = l x
forall x. l x
forall (rep :: * -> *) x. GBoundedMeasure rep => rep x
gmaxBound l x -> r x -> (:*:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: r x
forall x. r x
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 = String -> (:+:) l r x
forall a. HasCallStack => String -> a
Prelude.error String
"GBoundedMeasure :+:"