-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | Exact rational multiples of pi (and integer powers of pi)
--   
--   Provides an exact representation for rational multiples of pi
--   alongside an approximate representation of all reals. Useful for
--   storing and computing with conversion factors between physical units.
@package exact-pi
@version 0.5.0.2

-- | This type is sufficient to exactly express the closure of Q ∪ {π}
--   under multiplication and division. As a result it is useful for
--   representing conversion factors between physical units. Approximate
--   values are included both to close the remainder of the arithmetic
--   operations in the Num typeclass and to encode conversion
--   factors defined experimentally.
module Data.ExactPi

-- | Represents an exact or approximate real value. The exactly
--   representable values are rational multiples of an integer power of pi.
data ExactPi

-- | Exact z q = q * pi^z. Note that this means there are
--   many representations of zero.
Exact :: Integer -> Rational -> ExactPi

-- | An approximate value. This representation was chosen because it allows
--   conversion to floating types using their native definition of
--   pi.
Approximate :: (forall a. Floating a => a) -> ExactPi

-- | Approximates an exact or approximate value, converting it to a
--   Floating type. This uses the value of pi supplied by the
--   destination type, to provide the appropriate precision.
approximateValue :: Floating a => ExactPi -> a

-- | Identifies whether an ExactPi is an exact or approximate
--   representation of zero.
isZero :: ExactPi -> Bool

-- | Identifies whether an ExactPi is an exact value.
isExact :: ExactPi -> Bool

-- | Identifies whether an ExactPi is an exact representation of
--   zero.
isExactZero :: ExactPi -> Bool

-- | Identifies whether an ExactPi is an exact representation of
--   one.
isExactOne :: ExactPi -> Bool

-- | Identifies whether two ExactPi values are exactly equal.
areExactlyEqual :: ExactPi -> ExactPi -> Bool

-- | Identifies whether an ExactPi is an exact representation of an
--   integer.
isExactInteger :: ExactPi -> Bool

-- | Converts an ExactPi to an exact Integer or
--   Nothing.
toExactInteger :: ExactPi -> Maybe Integer

-- | Identifies whether an ExactPi is an exact representation of a
--   rational.
isExactRational :: ExactPi -> Bool

-- | Converts an ExactPi to an exact Rational or
--   Nothing.
toExactRational :: ExactPi -> Maybe Rational

-- | Converts an ExactPi to a list of increasingly accurate rational
--   approximations. Note that Approximate values are converted
--   using the Real instance for Double into a singleton
--   list. Note that exact rationals are also converted into a singleton
--   list.
--   
--   Implementation is based on Chudnovsky's algorithm.
rationalApproximations :: ExactPi -> [Rational]

-- | Given an infinite converging sequence of rationals, find their limit.
--   Takes a comparison function to determine when convergence is close
--   enough.
--   
--   
--   >>> getRationalLimit (==) (rationalApproximations (Exact 1 1)) :: Double
--   3.141592653589793
--   
getRationalLimit :: Fractional a => (a -> a -> Bool) -> [Rational] -> a
instance GHC.Internal.Float.Floating Data.ExactPi.ExactPi
instance GHC.Internal.Real.Fractional Data.ExactPi.ExactPi
instance GHC.Internal.Base.Monoid Data.ExactPi.ExactPi
instance GHC.Internal.Num.Num Data.ExactPi.ExactPi
instance GHC.Internal.Base.Semigroup Data.ExactPi.ExactPi
instance GHC.Internal.Show.Show Data.ExactPi.ExactPi

-- | This kind is sufficient to exactly express the closure of Q⁺ ∪ {π}
--   under multiplication and division. As a result it is useful for
--   representing conversion factors between physical units.
module Data.ExactPi.TypeLevel

-- | A type-level representation of a non-negative rational multiple of an
--   integer power of pi.
--   
--   Each type in this kind can be exactly represented at the term level by
--   a value of type ExactPi, provided that its denominator is
--   non-zero.
--   
--   Note that there are many representations of zero, and many
--   representations of dividing by zero. These are not excluded because
--   doing so introduces a lot of extra machinery. Play nice! Future
--   versions may not include a representation for zero.
--   
--   Of course there are also many representations of every value, because
--   the numerator need not be comprime to the denominator. For many
--   purposes it is not necessary to maintain the types in reduced form,
--   they will be appropriately reduced when converted to terms.
data ExactPi'
ExactPi' :: TypeInt -> Nat -> Nat -> ExactPi'

-- | A KnownDimension is one for which we can construct a term-level
--   representation.
--   
--   Each validly constructed type of kind ExactPi' has a
--   KnownExactPi instance, provided that its denominator is
--   non-zero.
class KnownExactPi (v :: ExactPi')

-- | Converts an ExactPi' type to an ExactPi value.
exactPiVal :: KnownExactPi v => Proxy v -> ExactPi

-- | Forms the product of ExactPi' types (in the arithmetic sense).
type family (a :: ExactPi') * (b :: ExactPi') :: ExactPi'

-- | Forms the quotient of ExactPi' types (in the arithmetic sense).
type family (a :: ExactPi') / (b :: ExactPi') :: ExactPi'

-- | Forms the reciprocal of an ExactPi' type.
type family Recip (a :: ExactPi') :: ExactPi'

-- | Converts a type-level natural to an ExactPi' type.
type ExactNatural (n :: Nat) = 'ExactPi' 'Zero n 1

-- | The ExactPi' type representing the number 1.
type One = ExactNatural 1

-- | The ExactPi' type representing the number pi.
type Pi = 'ExactPi' 'Pos1 1 1
type MinCtxt (v :: ExactPi') a = (KnownExactPi v, MinCtxt' v a, KnownMinCtxt MinCtxt' v)

-- | Determines the minimum context required for a numeric type to hold the
--   value associated with a specific ExactPi' type.
type family MinCtxt' (v :: ExactPi') :: Type -> Constraint

-- | Converts an ExactPi' type to a numeric value with the minimum
--   required context.
--   
--   When the value is known to be an integer, it can be returned as any
--   instance of Num. Similarly, rationals require
--   Fractional, and values that involve pi require
--   Floating.
injMin :: forall (v :: ExactPi') a. MinCtxt v a => Proxy v -> a
instance (Numeric.NumType.DK.Integers.KnownTypeInt z, GHC.Internal.TypeNats.KnownNat p, GHC.Internal.TypeNats.KnownNat q, 1 GHC.Internal.Data.Type.Ord.<= q) => Data.ExactPi.TypeLevel.KnownExactPi ('Data.ExactPi.TypeLevel.ExactPi' z p q)
instance Data.ExactPi.TypeLevel.KnownMinCtxt GHC.Internal.Float.Floating
instance Data.ExactPi.TypeLevel.KnownMinCtxt GHC.Internal.Real.Fractional
instance Data.ExactPi.TypeLevel.KnownMinCtxt GHC.Internal.Num.Num
