Safe Haskell	Safe
Language	Haskell2010

Type.Data.Num.Decimal.Number

Synopsis

Documentation

data Decimal Source

Representation name for decimal type level numbers.

Instances

Representation Decimal Source
type One Decimal Source

decimal :: Proxy n -> Proxy (Dec n) Source

data Dec x Source

The wrapper type for decimal type level numbers.

Instances

Integer x => Integer (Dec x) Source
(:/=:) x y => (Dec x) :/=: (Dec y) Source
(:==:) x y => (Dec x) :==: (Dec y) Source
(:>:) x y => (Dec x) :>: (Dec y) Source
(:>=:) x y => (Dec x) :>=: (Dec y) Source
(:<=:) x y => (Dec x) :<=: (Dec y) Source
(:<:) x y => (Dec x) :<: (Dec y) Source
type Repr (Dec x) = Decimal Source
type Log2Ceil (Dec x) = Dec (Log2Ceil x) Source
type Pow2 (Dec x) = Dec (Pow2 x) Source
type Div2 (Dec x) Source
type Mul2 (Dec x) = Dec ((:+:) x x) Source
type IsEven (Dec x) = IsEven x Source
type Pred (Dec x) = Dec (Pred x) Source
type Succ (Dec x) = Dec (Succ x) Source
type IsNatural (Dec x) Source
type IsNegative (Dec x) Source
type IsZero (Dec x) Source
type IsPositive (Dec x) Source
type Negate (Dec x) Source
type Compare (Dec x) (Dec y) = Compare x y Source
type (Dec x) :: (Dec y) = Dec ((::) x y) Source
type (Dec x) :-: (Dec y) = Dec ((:-:) x y) Source
type (Dec x) :+: (Dec y) = Dec ((:+:) x y) Source

data Zero Source

Instances

Natural Zero Source
Integer Zero Source
Zero :==: Zero Source
Zero :>=: Zero Source
Zero :<=: Zero Source
Zero :/=: (Pos y ys) Source
Zero :/=: (Neg y ys) Source
Zero :>: (Neg y ys) Source
Zero :>=: (Neg y ys) Source
Zero :<=: (Pos y ys) Source
Zero :<: (Pos y ys) Source
(Pos x xs) :/=: Zero Source
(Neg x xs) :/=: Zero Source
(Pos x xs) :>: Zero Source
(Pos x xs) :>=: Zero Source
(Neg x xs) :<=: Zero Source
(Neg x xs) :<: Zero Source
type ToUnary Zero = Zero Source
type Pow2 Zero Source
type IsEven Zero = True Source
type Pred Zero = Neg Dec1 EndDesc Source
type Succ Zero Source
type Compare Zero Zero = EQ Source
type Zero :*: _y = Zero Source
type Zero :+: y = y Source
type Compare Zero (Pos _y _ys) = LT Source
type Compare Zero (Neg _y _ys) = GT Source
type Compare (Pos _x _xs) Zero = GT Source
type Compare (Neg _x _xs) Zero = LT Source
type (Pos _x _xs) :*: Zero = Zero Source
type (Neg _x _xs) :*: Zero = Zero Source
type (Pos x xs) :+: Zero = Pos x xs Source
type (Neg x xs) :+: Zero = Neg x xs Source

data Pos x xs Source

Instances

Zero :/=: (Pos y ys) Source
Zero :<=: (Pos y ys) Source
Zero :<: (Pos y ys) Source
(Pos x, Digits xs) => Positive (Pos x xs) Source
(Pos x, Digits xs) => Natural (Pos x xs) Source
(Pos x, Digits xs) => Integer (Pos x xs) Source
(Pos x xs) :/=: Zero Source
(Pos x xs) :>: Zero Source
(Pos x xs) :>=: Zero Source
(~) * (IsEQ (ComparePos x xs y ys)) False => (Pos x xs) :/=: (Pos y ys) Source
(Pos x xs) :/=: (Neg y ys) Source
(Neg x xs) :/=: (Pos y ys) Source
(~) * (ComparePos x xs y ys) EQ => (Pos x xs) :==: (Pos y ys) Source
(~) * (ComparePos x xs y ys) GT => (Pos x xs) :>: (Pos y ys) Source
(Pos x xs) :>: (Neg y ys) Source
(~) * (GreaterPos y ys x xs) False => (Pos x xs) :>=: (Pos y ys) Source
(Pos x xs) :>=: (Neg y ys) Source
(~) * (GreaterPos x xs y ys) False => (Pos x xs) :<=: (Pos y ys) Source
(Neg x xs) :<=: (Pos y ys) Source
(~) * (ComparePos x xs y ys) LT => (Pos x xs) :<: (Pos y ys) Source
(Neg x xs) :<: (Pos y ys) Source
type Compare Zero (Pos _y _ys) = LT Source
type ToUnary (Pos x xs) = ToUnaryAcc (ToUnary x) xs Source
type Log2Ceil (Pos x xs) Source
type Pow2 (Pos x xs) Source
type IsEven (Pos x xs) Source
type Pred (Pos x xs) Source
type Succ (Pos x xs) Source
type Compare (Pos _x _xs) Zero = GT Source
type (Pos _x _xs) :*: Zero = Zero Source
type (Pos x xs) :+: Zero = Pos x xs Source
type Compare (Pos _x _xs) (Neg _y _ys) = GT Source
type Compare (Pos x xs) (Pos y ys) Source
type Compare (Neg _x _xs) (Pos _y _ys) = LT Source
type (Pos x xs) :*: (Neg y ys) Source
type (Pos x xs) :*: (Pos y ys) Source
type (Neg x xs) :*: (Pos y ys) Source
type (Pos x xs) :+: (Neg y ys) Source
type (Pos x xs) :+: (Pos y ys) Source
type (Neg x xs) :+: (Pos y ys) Source

data Neg x xs Source

Instances

Zero :/=: (Neg y ys) Source
Zero :>: (Neg y ys) Source
Zero :>=: (Neg y ys) Source
(Pos x, Digits xs) => Negative (Neg x xs) Source
(Pos x, Digits xs) => Integer (Neg x xs) Source
(Neg x xs) :/=: Zero Source
(Neg x xs) :<=: Zero Source
(Neg x xs) :<: Zero Source
(Pos x xs) :/=: (Neg y ys) Source
(~) * (IsEQ (ComparePos x xs y ys)) False => (Neg x xs) :/=: (Neg y ys) Source
(Neg x xs) :/=: (Pos y ys) Source
(~) * (ComparePos x xs y ys) EQ => (Neg x xs) :==: (Neg y ys) Source
(Pos x xs) :>: (Neg y ys) Source
(~) * (ComparePos x xs y ys) LT => (Neg x xs) :>: (Neg y ys) Source
(Pos x xs) :>=: (Neg y ys) Source
(~) * (GreaterPos x xs y ys) False => (Neg x xs) :>=: (Neg y ys) Source
(~) * (GreaterPos y ys x xs) False => (Neg x xs) :<=: (Neg y ys) Source
(Neg x xs) :<=: (Pos y ys) Source
(~) * (ComparePos x xs y ys) GT => (Neg x xs) :<: (Neg y ys) Source
(Neg x xs) :<: (Pos y ys) Source
type Compare Zero (Neg _y _ys) = GT Source
type IsEven (Neg x xs) Source
type Pred (Neg x xs) Source
type Succ (Neg x xs) Source
type Compare (Neg _x _xs) Zero = LT Source
type (Neg _x _xs) :*: Zero = Zero Source
type (Neg x xs) :+: Zero = Neg x xs Source
type Compare (Pos _x _xs) (Neg _y _ys) = GT Source
type Compare (Neg _x _xs) (Pos _y _ys) = LT Source
type Compare (Neg x xs) (Neg y ys) Source
type (Pos x xs) :*: (Neg y ys) Source
type (Neg x xs) :*: (Pos y ys) Source
type (Neg x xs) :*: (Neg y ys) Source
type (Pos x xs) :+: (Neg y ys) Source
type (Neg x xs) :+: (Pos y ys) Source
type (Neg x xs) :+: (Neg y ys) Source

data EndAsc Source

The terminator type for ascending decimal digit lists.

Instances

Show EndAsc Source

data ds :< d infixl 9 Source

data EndDesc Source

The terminator type for descending decimal digit lists.

Instances

Show EndDesc Source
Digits EndDesc Source
type ToUnaryAcc m EndDesc = m Source

data d :> ds infixr 9 Source

Instances

(C xh, Digits xl) => Digits ((:>) xh xl) Source
type ToUnaryAcc m ((:>) x xs) = ToUnaryAcc (UnaryAcc m x) xs Source

newtype Singleton x Source

Constructors

Singleton Integer

singleton :: Integer x => Singleton x Source

singletonFromProxy :: Integer n => Proxy n -> Singleton n Source

integerFromSingleton :: Integer n => Singleton n -> Integer Source

integralFromSingleton :: (Integer n, Num a) => Singleton n -> a Source

integralFromProxy :: (Integer n, Num a) => Proxy n -> a Source

class Integer n where Source

Methods

switch :: f Zero -> (forall x xs. (Pos x, Digits xs) => f (Neg x xs)) -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n Source

Instances

Integer Zero Source
(Pos x, Digits xs) => Integer (Pos x xs) Source
(Pos x, Digits xs) => Integer (Neg x xs) Source

class Integer n => Natural n where Source

Methods

switchNat :: f Zero -> (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n Source

Instances

Natural Zero Source
(Pos x, Digits xs) => Natural (Pos x xs) Source

class Natural n => Positive n where Source

Methods

switchPos :: (forall x xs. (Pos x, Digits xs) => f (Pos x xs)) -> f n Source

Instances

(Pos x, Digits xs) => Positive (Pos x xs) Source

class Integer n => Negative n where Source

Methods

switchNeg :: (forall x xs. (Pos x, Digits xs) => f (Neg x xs)) -> f n Source

Instances

(Pos x, Digits xs) => Negative (Neg x xs) Source

reifyIntegral :: Integer -> (forall s. Integer s => Proxy s -> w) -> w Source

reifyNatural :: Integer -> (forall s. Natural s => Proxy s -> a) -> Maybe a Source

reifyPositive :: Integer -> (forall s. Positive s => Proxy s -> a) -> Maybe a Source

reifyNegative :: Integer -> (forall s. Negative s => Proxy s -> a) -> Maybe a Source

reifyPos :: Integer -> (forall x xs. (Pos x, Digits xs) => Proxy (Pos x xs) -> a) -> Maybe a Source

reifyNeg :: Integer -> (forall x xs. (Pos x, Digits xs) => Proxy (Neg x xs) -> a) -> Maybe a Source

class Digits xs where Source

Methods

switchDigits :: f EndDesc -> (forall xh xl. (C xh, Digits xl) => f (xh :> xl)) -> f xs Source

Instances

Digits EndDesc Source
(C xh, Digits xl) => Digits ((:>) xh xl) Source

type family x :+: y Source

Instances

type Zero :+: y = y Source
type (Pos x xs) :+: Zero = Pos x xs Source
type (Neg x xs) :+: Zero = Neg x xs Source
type (Pos x xs) :+: (Neg y ys) Source
type (Pos x xs) :+: (Pos y ys) Source
type (Neg x xs) :+: (Pos y ys) Source
type (Neg x xs) :+: (Neg y ys) Source

type (:-:) x y = x :+: Negate y Source

type family x :*: y Source

Instances

type Zero :*: _y = Zero Source
type (Pos _x _xs) :*: Zero = Zero Source
type (Neg _x _xs) :*: Zero = Zero Source
type (Pos x xs) :*: (Neg y ys) Source
type (Pos x xs) :*: (Pos y ys) Source
type (Neg x xs) :*: (Pos y ys) Source
type (Neg x xs) :*: (Neg y ys) Source

type family Pred x Source

Instances

type Pred Zero = Neg Dec1 EndDesc Source
type Pred (Pos x xs) Source
type Pred (Neg x xs) Source

type family Succ x Source

Instances

type Succ Zero Source
type Succ (Pos x xs) Source
type Succ (Neg x xs) Source

type family Compare x y Source

Instances

type Compare Zero Zero = EQ Source
type Compare Zero (Pos _y _ys) = LT Source
type Compare Zero (Neg _y _ys) = GT Source
type Compare (Pos _x _xs) Zero = GT Source
type Compare (Neg _x _xs) Zero = LT Source
type Compare (Pos _x _xs) (Neg _y _ys) = GT Source
type Compare (Pos x xs) (Pos y ys) Source
type Compare (Neg _x _xs) (Pos _y _ys) = LT Source
type Compare (Neg x xs) (Neg y ys) Source

type family IsEven x Source

Instances

type IsEven Zero = True Source
type IsEven (Pos x xs) Source
type IsEven (Neg x xs) Source

type family Pow2 x Source

Instances

type Pow2 Zero Source
type Pow2 (Pos x xs) Source

type family Log2Ceil x Source

Instances

type Log2Ceil (Pos x xs) Source

class x :<: y Source

Instances

Zero :<: (Pos y ys) Source
(:<:) x y => (Dec x) :<: (Dec y) Source
(Neg x xs) :<: Zero Source
(~) * (ComparePos x xs y ys) LT => (Pos x xs) :<: (Pos y ys) Source
(~) * (ComparePos x xs y ys) GT => (Neg x xs) :<: (Neg y ys) Source
(Neg x xs) :<: (Pos y ys) Source

class x :<=: y Source

Instances

Zero :<=: Zero Source
Zero :<=: (Pos y ys) Source
(:<=:) x y => (Dec x) :<=: (Dec y) Source
(Neg x xs) :<=: Zero Source
(~) * (GreaterPos x xs y ys) False => (Pos x xs) :<=: (Pos y ys) Source
(~) * (GreaterPos y ys x xs) False => (Neg x xs) :<=: (Neg y ys) Source
(Neg x xs) :<=: (Pos y ys) Source

class x :==: y Source

Instances

Zero :==: Zero Source
(:==:) x y => (Dec x) :==: (Dec y) Source
(~) * (ComparePos x xs y ys) EQ => (Pos x xs) :==: (Pos y ys) Source
(~) * (ComparePos x xs y ys) EQ => (Neg x xs) :==: (Neg y ys) Source

class x :>: y Source

Instances

Zero :>: (Neg y ys) Source
(:>:) x y => (Dec x) :>: (Dec y) Source
(Pos x xs) :>: Zero Source
(~) * (ComparePos x xs y ys) GT => (Pos x xs) :>: (Pos y ys) Source
(Pos x xs) :>: (Neg y ys) Source
(~) * (ComparePos x xs y ys) LT => (Neg x xs) :>: (Neg y ys) Source

class x :>=: y Source

Instances

Zero :>=: Zero Source
Zero :>=: (Neg y ys) Source
(:>=:) x y => (Dec x) :>=: (Dec y) Source
(Pos x xs) :>=: Zero Source
(~) * (GreaterPos y ys x xs) False => (Pos x xs) :>=: (Pos y ys) Source
(Pos x xs) :>=: (Neg y ys) Source
(~) * (GreaterPos x xs y ys) False => (Neg x xs) :>=: (Neg y ys) Source

class x :/=: y Source

Instances

Zero :/=: (Pos y ys) Source
Zero :/=: (Neg y ys) Source
(:/=:) x y => (Dec x) :/=: (Dec y) Source
(Pos x xs) :/=: Zero Source
(Neg x xs) :/=: Zero Source
(~) * (IsEQ (ComparePos x xs y ys)) False => (Pos x xs) :/=: (Pos y ys) Source
(Pos x xs) :/=: (Neg y ys) Source
(~) * (IsEQ (ComparePos x xs y ys)) False => (Neg x xs) :/=: (Neg y ys) Source
(Neg x xs) :/=: (Pos y ys) Source

type family FromUnary n Source

Instances

type FromUnary Zero = Zero Source
type FromUnary (Succ n) = Succ (FromUnary n) Source

type family ToUnary n Source

Instances

type ToUnary Zero = Zero Source
type ToUnary (Pos x xs) = ToUnaryAcc (ToUnary x) xs Source

type family ToUnaryAcc m n Source

Instances

type ToUnaryAcc m EndDesc = m Source
type ToUnaryAcc m ((:>) x xs) = ToUnaryAcc (UnaryAcc m x) xs Source

type UnaryAcc m x = ToUnary x :+: (m :*: U10) Source