-- | Discretized floating point numbers, where the scaling factor is kept
-- as two phantom types denoting the rational number used for scaling.

module Numeric.Discretized where

import Control.Applicative
import Control.DeepSeq (NFData(..))
import Data.Aeson (FromJSON(..),ToJSON(..))
import Data.Binary (Binary)
import Data.Coerce
import Data.Hashable (Hashable)
import Data.Proxy
import Data.Ratio
import Data.Serialize (Serialize)
import Data.Vector.Unboxed.Deriving
import Debug.Trace
import GHC.Generics
import GHC.Real (Ratio(..))
import GHC.TypeLits

import Data.Info

import Algebra.Structure.Semiring
import Numeric.Limits



-- | Some discretizations are of the type @ln 2 / 2@ (@PAM@ matrices in Blast
-- for example). Using this type, we can annotate as follows: @Discretized
-- (RTyLn 2 :% RTyId 2)@.
--
-- One may use @Unknown@ if the scale is not known. For example, the blast
-- matrices use different scales internally and one needs to read the header to
-- get the scale.

data RatioTy a = RTyExp a | RTyId a | RTyLn a | RTyPlus (RatioTy a) (RatioTy a) | RTyTimes (RatioTy a) (RatioTy a) | Unknown

class RatioTyConstant a where
  ratioTyConstant ∷ Proxy a → Ratio Integer

instance (KnownNat k, KnownNat l) ⇒ RatioTyConstant (k :% l) where
  {-# Inline ratioTyConstant #-}
  ratioTyConstant :: Proxy (k ':% l) -> Ratio Integer
ratioTyConstant Proxy (k ':% l)
Proxy = let k :: Integer
k = Proxy k -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @k Proxy k
forall k (t :: k). Proxy t
Proxy; l :: Integer
l = Proxy l -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @l Proxy l
forall k (t :: k). Proxy t
Proxy in  Integer
k Integer -> Integer -> Ratio Integer
forall a. a -> a -> Ratio a
:% Integer
l

instance (KnownNat k) ⇒ RatioTyConstant (RTyExp (k∷Nat)) where
  {-# Inline ratioTyConstant #-}
  ratioTyConstant :: Proxy ('RTyExp k) -> Ratio Integer
ratioTyConstant Proxy ('RTyExp k)
Proxy = let n :: Integer
n = Proxy k -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @k Proxy k
forall k (t :: k). Proxy t
Proxy in Double -> Ratio Integer
forall a. Real a => a -> Ratio Integer
toRational (Double -> Double
forall a. Floating a => a -> a
exp (Double -> Double) -> Double -> Double
forall a b. (a -> b) -> a -> b
$ Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
n)

instance (KnownNat k) ⇒ RatioTyConstant (RTyId (k∷Nat)) where
  {-# Inline ratioTyConstant #-}
  ratioTyConstant :: Proxy ('RTyId k) -> Ratio Integer
ratioTyConstant Proxy ('RTyId k)
Proxy = let n :: Integer
n = Proxy k -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @k Proxy k
forall k (t :: k). Proxy t
Proxy in Integer -> Ratio Integer
forall a. Real a => a -> Ratio Integer
toRational Integer
n

instance (KnownNat k) ⇒ RatioTyConstant (RTyLn (k∷Nat)) where
  {-# Inline ratioTyConstant #-}
  ratioTyConstant :: Proxy ('RTyLn k) -> Ratio Integer
ratioTyConstant Proxy ('RTyLn k)
Proxy = let n :: Integer
n = Proxy k -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @k Proxy k
forall k (t :: k). Proxy t
Proxy in Double -> Ratio Integer
forall a. Real a => a -> Ratio Integer
toRational (Double -> Double
forall a. Floating a => a -> a
log (Double -> Double) -> Double -> Double
forall a b. (a -> b) -> a -> b
$ Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
n)

instance (RatioTyConstant a, RatioTyConstant b) ⇒ RatioTyConstant (RTyPlus (a∷RatioTy k) (b∷RatioTy k)) where
  {-# Inline ratioTyConstant #-}
  ratioTyConstant :: Proxy ('RTyPlus a b) -> Ratio Integer
ratioTyConstant Proxy ('RTyPlus a b)
Proxy = Proxy a -> Ratio Integer
forall k (a :: k). RatioTyConstant a => Proxy a -> Ratio Integer
ratioTyConstant @a Proxy a
forall k (t :: k). Proxy t
Proxy Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Num a => a -> a -> a
+ Proxy b -> Ratio Integer
forall k (a :: k). RatioTyConstant a => Proxy a -> Ratio Integer
ratioTyConstant @b Proxy b
forall k (t :: k). Proxy t
Proxy

instance (RatioTyConstant a, RatioTyConstant b) ⇒ RatioTyConstant (RTyTimes (a∷RatioTy k) (b∷RatioTy k)) where
  {-# Inline ratioTyConstant #-}
  ratioTyConstant :: Proxy ('RTyTimes a b) -> Ratio Integer
ratioTyConstant Proxy ('RTyTimes a b)
Proxy = Proxy a -> Ratio Integer
forall k (a :: k). RatioTyConstant a => Proxy a -> Ratio Integer
ratioTyConstant @a Proxy a
forall k (t :: k). Proxy t
Proxy Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Num a => a -> a -> a
* Proxy b -> Ratio Integer
forall k (a :: k). RatioTyConstant a => Proxy a -> Ratio Integer
ratioTyConstant @b Proxy b
forall k (t :: k). Proxy t
Proxy

-- | A discretized value takes a floating point number @n@ and produces a
-- discretized value. The actual discretization formula is given on the type
-- level, freeing us from having to carry around some scaling function.
--
-- Typically, one might use types likes @100@, @(100 :% 1)@, or @(RTyLn 2 :%
-- RTyId 2)@.
--
-- The main use of a 'Discretized' value is to enable calculations with 'Int'
-- while somewhat pretending to use floating point values.
--
-- Be careful with certain operations like @(*)@ as they will easily cause the
-- numbers to arbitrarily wrong. @(+)@ and @(-)@ are fine, however.
--
-- NOTE Export and import of data is in the form of floating points, which can
-- lead to additional loss of precision if one is careless!
--
-- TODO fast 'Show' methods required!
--
-- TODO blaze stuff?
--
-- TODO We might want to discretize @LogDomain@ style values. This requires
-- some thought on in which direction to wrap. Maybe, we want to log-domain
-- Discretized values, which probably just works.

newtype Discretized (b ∷ k) = Discretized { Discretized b -> Int
getDiscretized ∷ Int }
  deriving (Discretized b -> Discretized b -> Bool
(Discretized b -> Discretized b -> Bool)
-> (Discretized b -> Discretized b -> Bool) -> Eq (Discretized b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (b :: k). Discretized b -> Discretized b -> Bool
/= :: Discretized b -> Discretized b -> Bool
$c/= :: forall k (b :: k). Discretized b -> Discretized b -> Bool
== :: Discretized b -> Discretized b -> Bool
$c== :: forall k (b :: k). Discretized b -> Discretized b -> Bool
Eq,Eq (Discretized b)
Eq (Discretized b)
-> (Discretized b -> Discretized b -> Ordering)
-> (Discretized b -> Discretized b -> Bool)
-> (Discretized b -> Discretized b -> Bool)
-> (Discretized b -> Discretized b -> Bool)
-> (Discretized b -> Discretized b -> Bool)
-> (Discretized b -> Discretized b -> Discretized b)
-> (Discretized b -> Discretized b -> Discretized b)
-> Ord (Discretized b)
Discretized b -> Discretized b -> Bool
Discretized b -> Discretized b -> Ordering
Discretized b -> Discretized b -> Discretized b
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (b :: k). Eq (Discretized b)
forall k (b :: k). Discretized b -> Discretized b -> Bool
forall k (b :: k). Discretized b -> Discretized b -> Ordering
forall k (b :: k). Discretized b -> Discretized b -> Discretized b
min :: Discretized b -> Discretized b -> Discretized b
$cmin :: forall k (b :: k). Discretized b -> Discretized b -> Discretized b
max :: Discretized b -> Discretized b -> Discretized b
$cmax :: forall k (b :: k). Discretized b -> Discretized b -> Discretized b
>= :: Discretized b -> Discretized b -> Bool
$c>= :: forall k (b :: k). Discretized b -> Discretized b -> Bool
> :: Discretized b -> Discretized b -> Bool
$c> :: forall k (b :: k). Discretized b -> Discretized b -> Bool
<= :: Discretized b -> Discretized b -> Bool
$c<= :: forall k (b :: k). Discretized b -> Discretized b -> Bool
< :: Discretized b -> Discretized b -> Bool
$c< :: forall k (b :: k). Discretized b -> Discretized b -> Bool
compare :: Discretized b -> Discretized b -> Ordering
$ccompare :: forall k (b :: k). Discretized b -> Discretized b -> Ordering
$cp1Ord :: forall k (b :: k). Eq (Discretized b)
Ord,(forall x. Discretized b -> Rep (Discretized b) x)
-> (forall x. Rep (Discretized b) x -> Discretized b)
-> Generic (Discretized b)
forall x. Rep (Discretized b) x -> Discretized b
forall x. Discretized b -> Rep (Discretized b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (b :: k) x. Rep (Discretized b) x -> Discretized b
forall k (b :: k) x. Discretized b -> Rep (Discretized b) x
$cto :: forall k (b :: k) x. Rep (Discretized b) x -> Discretized b
$cfrom :: forall k (b :: k) x. Discretized b -> Rep (Discretized b) x
Generic,ReadPrec [Discretized b]
ReadPrec (Discretized b)
Int -> ReadS (Discretized b)
ReadS [Discretized b]
(Int -> ReadS (Discretized b))
-> ReadS [Discretized b]
-> ReadPrec (Discretized b)
-> ReadPrec [Discretized b]
-> Read (Discretized b)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall k (b :: k). ReadPrec [Discretized b]
forall k (b :: k). ReadPrec (Discretized b)
forall k (b :: k). Int -> ReadS (Discretized b)
forall k (b :: k). ReadS [Discretized b]
readListPrec :: ReadPrec [Discretized b]
$creadListPrec :: forall k (b :: k). ReadPrec [Discretized b]
readPrec :: ReadPrec (Discretized b)
$creadPrec :: forall k (b :: k). ReadPrec (Discretized b)
readList :: ReadS [Discretized b]
$creadList :: forall k (b :: k). ReadS [Discretized b]
readsPrec :: Int -> ReadS (Discretized b)
$creadsPrec :: forall k (b :: k). Int -> ReadS (Discretized b)
Read)

instance Show (Discretized b) where
  show :: Discretized b -> String
show (Discretized Int
d) = Int -> String
forall a. Show a => a -> String
show Int
d

instance Info (Discretized b) where
  -- TODO show @b@ information
  info :: Discretized b -> String
info = Int -> String
forall a. Show a => a -> String
show (Int -> String)
-> (Discretized b -> Int) -> Discretized b -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Discretized b -> Int
forall k (b :: k). Discretized b -> Int
getDiscretized

fromUnknown ∷ Discretized Unknown → Discretized t
{-# Inline fromUnknown #-}
fromUnknown :: Discretized 'Unknown -> Discretized t
fromUnknown = Discretized 'Unknown -> Discretized t
coerce

derivingUnbox "Discretized"
  [t| forall t . Discretized t → Int |]  [| getDiscretized |]  [| Discretized |]

instance NFData (Discretized t) where
  rnf :: Discretized t -> ()
rnf (Discretized Int
k) = Int -> ()
forall a. NFData a => a -> ()
rnf Int
k
  {-# Inline rnf #-}

instance Binary    (Discretized t)
instance Serialize (Discretized t)
instance Hashable  (Discretized t)

instance (KnownNat k, KnownNat l) ⇒ ToJSON (Discretized (k :% l)) where
  toJSON :: Discretized (k ':% l) -> Value
toJSON = Double -> Value
forall a. ToJSON a => a -> Value
toJSON (Double -> Value)
-> (Discretized (k ':% l) -> Double)
-> Discretized (k ':% l)
-> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fractional Double => Ratio Integer -> Double
forall a. Fractional a => Ratio Integer -> a
fromRational @Double (Ratio Integer -> Double)
-> (Discretized (k ':% l) -> Ratio Integer)
-> Discretized (k ':% l)
-> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Discretized (k ':% l) -> Ratio Integer
forall a. Real a => a -> Ratio Integer
toRational

instance (KnownNat k, KnownNat l) ⇒ FromJSON (Discretized (k :% l)) where
  parseJSON :: Value -> Parser (Discretized (k ':% l))
parseJSON = (Double -> Discretized (k ':% l))
-> Parser Double -> Parser (Discretized (k ':% l))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ratio Integer -> Discretized (k ':% l)
forall a. Fractional a => Ratio Integer -> a
fromRational (Ratio Integer -> Discretized (k ':% l))
-> (Double -> Ratio Integer) -> Double -> Discretized (k ':% l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Real Double => Double -> Ratio Integer
forall a. Real a => a -> Ratio Integer
toRational @Double) (Parser Double -> Parser (Discretized (k ':% l)))
-> (Value -> Parser Double)
-> Value
-> Parser (Discretized (k ':% l))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Parser Double
forall a. FromJSON a => Value -> Parser a
parseJSON

instance Num (Discretized Unknown) where
  Discretized Int
x + :: Discretized 'Unknown
-> Discretized 'Unknown -> Discretized 'Unknown
+ Discretized Int
y = Int -> Discretized 'Unknown
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Discretized 'Unknown) -> Int -> Discretized 'Unknown
forall a b. (a -> b) -> a -> b
$ Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y
  Discretized Int
x - :: Discretized 'Unknown
-> Discretized 'Unknown -> Discretized 'Unknown
- Discretized Int
y = Int -> Discretized 'Unknown
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Discretized 'Unknown) -> Int -> Discretized 'Unknown
forall a b. (a -> b) -> a -> b
$ Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
y
  * :: Discretized 'Unknown
-> Discretized 'Unknown -> Discretized 'Unknown
(*) = String
-> Discretized 'Unknown
-> Discretized 'Unknown
-> Discretized 'Unknown
forall a. HasCallStack => String -> a
error String
"Discretized Unknown does not admit (*)"
  abs :: Discretized 'Unknown -> Discretized 'Unknown
abs (Discretized Int
x) = Int -> Discretized 'Unknown
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Discretized 'Unknown) -> Int -> Discretized 'Unknown
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Num a => a -> a
abs Int
x
  signum :: Discretized 'Unknown -> Discretized 'Unknown
signum (Discretized Int
x) = Int -> Discretized 'Unknown
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Discretized 'Unknown) -> Int -> Discretized 'Unknown
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Num a => a -> a
signum Int
x
  fromInteger :: Integer -> Discretized 'Unknown
fromInteger = String -> Integer -> Discretized 'Unknown
forall a. HasCallStack => String -> a
error String
"Discretized Unknown does not admit fromInteger"
  {-# Inline (+) #-}
  {-# Inline (-) #-}
  {-# Inline abs #-}
  {-# Inline signum #-}

instance (KnownNat u, KnownNat l) ⇒ Num (Discretized ((u∷Nat) :% (l∷Nat))) where
  {-# Inline (+) #-}
  Discretized Int
x + :: Discretized (u ':% l)
-> Discretized (u ':% l) -> Discretized (u ':% l)
+ Discretized Int
y = Int -> Discretized (u ':% l)
forall k (b :: k). Int -> Discretized b
Discretized (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y)
  {-# Inline (-) #-}
  Discretized Int
x - :: Discretized (u ':% l)
-> Discretized (u ':% l) -> Discretized (u ':% l)
- Discretized Int
y = Int -> Discretized (u ':% l)
forall k (b :: k). Int -> Discretized b
Discretized (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
y)
  -- TODO it should be possible to generalize this over arbitrary value, or
  -- replace @KnownNat@ with the above @ratioTyConstant@.
  {-# Inline (*) #-}
  Discretized Int
x * :: Discretized (u ':% l)
-> Discretized (u ':% l) -> Discretized (u ':% l)
* Discretized Int
y =
    let u :: Int
u = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy u -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @u Proxy u
forall k (t :: k). Proxy t
Proxy
        l :: Int
l = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy l -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @l Proxy l
forall k (t :: k). Proxy t
Proxy
    in  Int -> Discretized (u ':% l)
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Discretized (u ':% l)) -> Int -> Discretized (u ':% l)
forall a b. (a -> b) -> a -> b
$ (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
yInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
u) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
l
  {-# Inline abs #-}
  abs :: Discretized (u ':% l) -> Discretized (u ':% l)
abs (Discretized Int
x) = Int -> Discretized (u ':% l)
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Int
forall a. Num a => a -> a
abs Int
x)
  {-# Inline signum #-}
  signum :: Discretized (u ':% l) -> Discretized (u ':% l)
signum (Discretized Int
x) = Int -> Discretized (u ':% l)
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Discretized (u ':% l)) -> Int -> Discretized (u ':% l)
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Num a => a -> a
signum Int
x
  {-# Inline fromInteger #-}
  fromInteger :: Integer -> Discretized (u ':% l)
fromInteger Integer
x =
    let u :: Int
u = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy u -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @u Proxy u
forall k (t :: k). Proxy t
Proxy
        l :: Int
l = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy l -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @l Proxy l
forall k (t :: k). Proxy t
Proxy
    in  Int -> Discretized (u ':% l)
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Discretized (u ':% l)) -> Int -> Discretized (u ':% l)
forall a b. (a -> b) -> a -> b
$ (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
xInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
u) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
l

instance Enum (Discretized b) where
  toEnum :: Int -> Discretized b
toEnum = Int -> Discretized b
forall k (b :: k). Int -> Discretized b
Discretized
  {-# Inline toEnum #-}
  fromEnum :: Discretized b -> Int
fromEnum = Discretized b -> Int
forall k (b :: k). Discretized b -> Int
getDiscretized
  {-# Inline fromEnum #-}

-- instance (Enum (Discretized b), KnownNat u, KnownNat l) ⇒ Integral (Discretized u l) where

instance (KnownNat u, KnownNat l) ⇒ Fractional (Discretized ((u∷Nat) :% (l∷Nat))) where
  {-# Inline (/) #-}
  Discretized Int
x / :: Discretized (u ':% l)
-> Discretized (u ':% l) -> Discretized (u ':% l)
/ Discretized Int
y =
    let u :: Int
u = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy u -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @u Proxy u
forall k (t :: k). Proxy t
Proxy
        l :: Int
l = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Proxy l -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @l Proxy l
forall k (t :: k). Proxy t
Proxy
    in  Int -> Discretized (u ':% l)
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Discretized (u ':% l)) -> Int -> Discretized (u ':% l)
forall a b. (a -> b) -> a -> b
$ (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
l) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` (Int
y Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
u)
  {-# Inline recip #-}
  recip :: Discretized (u ':% l) -> Discretized (u ':% l)
recip (Discretized Int
x) =
    let u :: Integer
u = Integer -> Integer
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy u -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @u Proxy u
forall k (t :: k). Proxy t
Proxy
        l :: Integer
l = Integer -> Integer
forall a. Num a => Integer -> a
fromInteger (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy l -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @l Proxy l
forall k (t :: k). Proxy t
Proxy
    in  String -> Discretized (u ':% l)
forall a. HasCallStack => String -> a
error String
"need to find approximately ok transformation"
  {-# Inline fromRational #-}
  fromRational :: Ratio Integer -> Discretized (u ':% l)
fromRational (Integer
a :% Integer
b) =
    let u :: Integer
u = Proxy u -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @u Proxy u
forall k (t :: k). Proxy t
Proxy
        l :: Integer
l = Proxy l -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @l Proxy l
forall k (t :: k). Proxy t
Proxy
    in  Int -> Discretized (u ':% l)
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Discretized (u ':% l))
-> (Integer -> Int) -> Integer -> Discretized (u ':% l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Discretized (u ':% l))
-> Integer -> Discretized (u ':% l)
forall a b. (a -> b) -> a -> b
$ (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
l) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` (Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
u)

instance (KnownNat u, KnownNat l) ⇒ Real (Discretized ((u∷Nat) :% (l∷Nat))) where
  {-# Inline toRational #-}
  toRational :: Discretized (u ':% l) -> Ratio Integer
toRational (Discretized Int
d) =
    let u :: Integer
u = Proxy u -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @u Proxy u
forall k (t :: k). Proxy t
Proxy
        l :: Integer
l = Proxy l -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @l Proxy l
forall k (t :: k). Proxy t
Proxy
    in  (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
d Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
u) Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
l

instance (Num (Discretized k)) ⇒ Semiring (Discretized k) where
  plus :: Discretized k -> Discretized k -> Discretized k
plus = Discretized k -> Discretized k -> Discretized k
forall a. Num a => a -> a -> a
(+)
  times :: Discretized k -> Discretized k -> Discretized k
times = Discretized k -> Discretized k -> Discretized k
forall a. Num a => a -> a -> a
(*)
  zero :: Discretized k
zero = Discretized k
0
  one :: Discretized k
one = Discretized k
1
  {-# Inline plus  #-}
  {-# Inline times #-}
  {-# Inline zero  #-}
  {-# Inline one   #-}

instance (NumericLimits (Discretized t)) where
  minFinite :: Discretized t
minFinite = Int -> Discretized t
forall k (b :: k). Int -> Discretized b
Discretized Int
forall x. NumericLimits x => x
minFinite
  {-# Inline minFinite #-}
  maxFinite :: Discretized t
maxFinite = Int -> Discretized t
forall k (b :: k). Int -> Discretized b
Discretized Int
forall x. NumericLimits x => x
maxFinite
  {-# Inline maxFinite #-}

-- | Discretizes any @Real a@ into the @Discretized@ value. This conversion
-- is /lossy/ and uses a type-level rational of @u :% l@!

discretizeRatio ∷ forall a u l . (Real a, KnownNat u, KnownNat l) ⇒ a → Discretized ((u∷Nat) :% (l∷Nat))
{-# Inline discretizeRatio #-}
discretizeRatio :: a -> Discretized (u ':% l)
discretizeRatio a
a =
  let u :: Integer
u = Proxy u -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @u Proxy u
forall k (t :: k). Proxy t
Proxy
      l :: Integer
l = Proxy l -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal @l Proxy l
forall k (t :: k). Proxy t
Proxy
      k :: Ratio Integer
k = a -> Ratio Integer
forall a. Real a => a -> Ratio Integer
toRational a
a
  in  Int -> Discretized (u ':% l)
forall k (b :: k). Int -> Discretized b
Discretized (Int -> Discretized (u ':% l))
-> (Integer -> Int) -> Integer -> Discretized (u ':% l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Discretized (u ':% l))
-> Integer -> Discretized (u ':% l)
forall a b. (a -> b) -> a -> b
$ Ratio Integer -> Integer
forall a. Ratio a -> a
numerator Ratio Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
l Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` (Ratio Integer -> Integer
forall a. Ratio a -> a
denominator Ratio Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
u)