{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ > 805
{-# LANGUAGE NoStarIsType #-}
#endif
module Data.ExactPi.TypeLevel
(
type ExactPi'(..),
KnownExactPi(..),
type (*), type (/), type Recip,
type ExactNatural,
type One, type Pi,
type MinCtxt, type MinCtxt',
injMin
)
where
import Data.ExactPi
import Data.Maybe (fromJust)
import Data.Proxy
import Data.Ratio
import GHC.TypeLits hiding (type (*), type (^))
import qualified GHC.TypeLits as N
import Numeric.NumType.DK.Integers hiding (type (*), type (/))
import qualified Numeric.NumType.DK.Integers as Z
data ExactPi' = ExactPi' TypeInt
Nat
Nat
class KnownExactPi (v :: ExactPi') where
exactPiVal :: Proxy v -> ExactPi
type family MinCtxt' (v :: ExactPi') where
MinCtxt' ('ExactPi' 'Zero p 1) = Num
MinCtxt' ('ExactPi' 'Zero p q) = Fractional
MinCtxt' ('ExactPi' z p q) = Floating
type MinCtxt v a = (KnownExactPi v, MinCtxt' v a, KnownMinCtxt (MinCtxt' v))
class KnownMinCtxt c where
inj :: c a => Proxy c
-> ExactPi
-> a
instance KnownMinCtxt Num where
inj :: Proxy Num -> ExactPi -> a
inj Proxy Num
_ = Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> (ExactPi -> Integer) -> ExactPi -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer -> Integer
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Integer -> Integer)
-> (ExactPi -> Maybe Integer) -> ExactPi -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExactPi -> Maybe Integer
toExactInteger
instance KnownMinCtxt Fractional where
inj :: Proxy Fractional -> ExactPi -> a
inj Proxy Fractional
_ = Rational -> a
forall a. Fractional a => Rational -> a
fromRational (Rational -> a) -> (ExactPi -> Rational) -> ExactPi -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Rational -> Rational
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Rational -> Rational)
-> (ExactPi -> Maybe Rational) -> ExactPi -> Rational
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExactPi -> Maybe Rational
toExactRational
instance KnownMinCtxt Floating where
inj :: Proxy Floating -> ExactPi -> a
inj Proxy Floating
_ = ExactPi -> a
forall a. Floating a => ExactPi -> a
approximateValue
injMin :: forall v a.(MinCtxt v a) => Proxy v -> a
injMin :: Proxy v -> a
injMin = Proxy (MinCtxt' v) -> ExactPi -> a
forall (c :: Type -> Constraint) a.
(KnownMinCtxt c, c a) =>
Proxy c -> ExactPi -> a
inj (Proxy (MinCtxt' v)
forall k (t :: k). Proxy t
Proxy :: Proxy (MinCtxt' v)) (ExactPi -> a) -> (Proxy v -> ExactPi) -> Proxy v -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy v -> ExactPi
forall (v :: ExactPi'). KnownExactPi v => Proxy v -> ExactPi
exactPiVal
instance (KnownTypeInt z, KnownNat p, KnownNat q, 1 <= q) => KnownExactPi ('ExactPi' z p q) where
exactPiVal :: Proxy ('ExactPi' z p q) -> ExactPi
exactPiVal Proxy ('ExactPi' z p q)
_ = Integer -> Rational -> ExactPi
Exact Integer
z' (Integer
p' Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
q')
where
z' :: Integer
z' = Proxy z -> Integer
forall (i :: TypeInt) a. (KnownTypeInt i, Num a) => Proxy i -> a
toNum (Proxy z
forall k (t :: k). Proxy t
Proxy :: Proxy z)
p' :: Integer
p' = Proxy p -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy p
forall k (t :: k). Proxy t
Proxy :: Proxy p)
q' :: Integer
q' = Proxy q -> Integer
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Integer
natVal (Proxy q
forall k (t :: k). Proxy t
Proxy :: Proxy q)
type family (a :: ExactPi') * (b :: ExactPi') :: ExactPi' where
('ExactPi' z p q) * ('ExactPi' z' p' q') = 'ExactPi' (z Z.+ z') (p N.* p') (q N.* q')
type family (a :: ExactPi') / (b :: ExactPi') :: ExactPi' where
('ExactPi' z p q) / ('ExactPi' z' p' q') = 'ExactPi' (z Z.- z') (p N.* q') (q N.* p')
type family Recip (a :: ExactPi') :: ExactPi' where
Recip ('ExactPi' z p q) = 'ExactPi' (Negate z) q p
type ExactNatural n = 'ExactPi' 'Zero n 1
type One = ExactNatural 1
type Pi = 'ExactPi' 'Pos1 1 1