Safe Haskell | None |
---|---|
Language | Haskell2010 |
promoted numeric functions
Synopsis
- data p + q
- data p - q
- data p * q
- data p / q
- data Negate p
- data Abs p
- data Signum p
- data FromInteger (t :: Type) p
- data FromInteger' t n
- data FromIntegral (t :: Type) p
- data FromIntegral' t n
- data Truncate (t :: Type) p
- data Truncate' t p
- data Ceiling (t :: Type) p
- data Ceiling' t p
- data Floor (t :: Type) p
- data Floor' t p
- data Even
- data Odd
- data Div p q
- data Mod p q
- data DivMod p q
- data QuotRem p q
- data Quot p q
- data Rem p q
- data LogBase p q
- data p ^ q
- data p ** q
- data p % q
- data p -% q
- data ToRational p
- data FromRational (t :: Type) p
- data FromRational' t r
- data ReadBase (t :: Type) (n :: Nat) p
- data ReadBase' t (n :: Nat) p
- data ShowBase (n :: Nat) p
numeric expressions
fractional division
>>>
pz @(Fst Id / Snd Id) (13,2)
PresentT 6.5
>>>
pz @(ToRational 13 / Id) 0
FailT "(/) zero denominator"
>>>
pz @(12 % 7 / 14 % 5 + Id) 12.4
PresentT (3188 % 245)
similar to negate
>>>
pz @(Negate Id) 14
PresentT (-14)
>>>
pz @(Negate (Fst Id * Snd Id)) (14,3)
PresentT (-42)
>>>
pz @(Negate (15 -% 4)) "abc"
PresentT (15 % 4)
>>>
pz @(Negate (15 % 3)) ()
PresentT ((-5) % 1)
>>>
pz @(Negate (Fst Id % Snd Id)) (14,3)
PresentT ((-14) % 3)
similar to abs
>>>
pz @(Abs Id) (-14)
PresentT 14
>>>
pz @(Abs (Snd Id)) ("xx",14)
PresentT 14
>>>
pz @(Abs Id) 0
PresentT 0
>>>
pz @(Abs (Negate 44)) "aaa"
PresentT 44
similar to signum
>>>
pz @(Signum Id) (-14)
PresentT (-1)
>>>
pz @(Signum Id) 14
PresentT 1
>>>
pz @(Signum Id) 0
PresentT 0
data FromInteger (t :: Type) p Source #
fromInteger
function where you need to provide the type 't' of the result
>>>
pz @(FromInteger (SG.Sum _) Id) 23
PresentT (Sum {getSum = 23})
>>>
pz @(FromInteger Rational 44) 12
PresentT (44 % 1)
>>>
pz @(FromInteger Rational Id) 12
PresentT (12 % 1)
>>>
pl @((FromInteger _ 12 &&& Id) >> Fst Id + Snd Id) (SG.Min 7)
Present Min {getMin = 19} ((>>) Min {getMin = 19} | {getMin = 19}) PresentT (Min {getMin = 19})
>>>
pl @((FromInteger _ 12 &&& Id) >> SapA) (SG.Product 7)
Present Product {getProduct = 84} ((>>) Product {getProduct = 84} | {getProduct = 84}) PresentT (Product {getProduct = 84})
>>>
pl @(FromInteger (SG.Sum _) (Fst Id)) (3,"A")
Present Sum {getSum = 3} (FromInteger Sum {getSum = 3}) PresentT (Sum {getSum = 3})
>>>
pl @(FromInteger DiffTime 123) 'x'
Present 123s (FromInteger 123s) PresentT 123s
Instances
P (FromIntegerT t p) x => P (FromInteger t p :: Type) x Source # | |
Defined in Predicate.Data.Numeric type PP (FromInteger t p) x :: Type Source # eval :: MonadEval m => proxy (FromInteger t p) -> POpts -> x -> m (TT (PP (FromInteger t p) x)) Source # | |
type PP (FromInteger t p :: Type) x Source # | |
Defined in Predicate.Data.Numeric |
data FromInteger' t n Source #
Instances
(Num (PP t a), Integral (PP n a), P n a, Show (PP t a)) => P (FromInteger' t n :: Type) a Source # | |
Defined in Predicate.Data.Numeric type PP (FromInteger' t n) a :: Type Source # eval :: MonadEval m => proxy (FromInteger' t n) -> POpts -> a -> m (TT (PP (FromInteger' t n) a)) Source # | |
type PP (FromInteger' t n :: Type) a Source # | |
Defined in Predicate.Data.Numeric |
data FromIntegral (t :: Type) p Source #
Instances
P (FromIntegralT t p) x => P (FromIntegral t p :: Type) x Source # | |
Defined in Predicate.Data.Numeric type PP (FromIntegral t p) x :: Type Source # eval :: MonadEval m => proxy (FromIntegral t p) -> POpts -> x -> m (TT (PP (FromIntegral t p) x)) Source # | |
type PP (FromIntegral t p :: Type) x Source # | |
Defined in Predicate.Data.Numeric |
data FromIntegral' t n Source #
fromIntegral
function where you need to provide the type 't' of the result
>>>
pz @(FromIntegral (SG.Sum _) Id) 23
PresentT (Sum {getSum = 23})
Instances
(Num (PP t a), Integral (PP n a), P n a, Show (PP t a), Show (PP n a)) => P (FromIntegral' t n :: Type) a Source # | |
Defined in Predicate.Data.Numeric type PP (FromIntegral' t n) a :: Type Source # eval :: MonadEval m => proxy (FromIntegral' t n) -> POpts -> a -> m (TT (PP (FromIntegral' t n) a)) Source # | |
type PP (FromIntegral' t n :: Type) a Source # | |
Defined in Predicate.Data.Numeric |
truncate
function where you need to provide the type 't' of the result
>>>
pz @(Truncate Int Id) (23 % 5)
PresentT 4
>>>
pl @(Truncate' (Fst Id >> Unproxy) (Snd Id)) (Proxy @Integer,2.3)
Present 2 (Truncate 2 | 2.3) PresentT 2
>>>
pl @(Truncate' (Fst Id) (Snd Id)) (1::Int,2.3)
Present 2 (Truncate 2 | 2.3) PresentT 2
ceiling
function where you need to provide the type 't' of the result
>>>
pz @(Ceiling Int Id) (23 % 5)
PresentT 5
floor
function where you need to provide the type 't' of the result
>>>
pz @(Floor Int Id) (23 % 5)
PresentT 4
similar to even
>>>
pz @(Map Even Id) [9,-4,12,1,2,3]
PresentT [False,True,True,False,True,False]
>>>
pz @(Map '(Even,Odd) Id) [9,-4,12,1,2,3]
PresentT [(False,True),(True,False),(True,False),(False,True),(True,False),(False,True)]
similar to div
>>>
pz @(Div (Fst Id) (Snd Id)) (10,4)
PresentT 2
>>>
pz @(Div (Fst Id) (Snd Id)) (10,0)
FailT "Div zero denominator"
similar to mod
>>>
pz @(Mod (Fst Id) (Snd Id)) (10,3)
PresentT 1
>>>
pz @(Mod (Fst Id) (Snd Id)) (10,0)
FailT "Mod zero denominator"
similar to divMod
>>>
pz @(DivMod (Fst Id) (Snd Id)) (10,3)
PresentT (3,1)
>>>
pz @(DivMod (Fst Id) (Snd Id)) (10,-3)
PresentT (-4,-2)
>>>
pz @(DivMod (Fst Id) (Snd Id)) (-10,3)
PresentT (-4,2)
>>>
pz @(DivMod (Fst Id) (Snd Id)) (-10,-3)
PresentT (3,-1)
>>>
pz @(DivMod (Fst Id) (Snd Id)) (10,0)
FailT "DivMod zero denominator"
>>>
pl @(DivMod (Negate Id) 7) 23
Present (-4,5) (-23 `divMod` 7 = (-4,5)) PresentT (-4,5)
>>>
pl @(DivMod (Fst Id) (Snd Id)) (10,-3)
Present (-4,-2) (10 `divMod` -3 = (-4,-2)) PresentT (-4,-2)
>>>
pl @(DivMod (Fst Id) (Snd Id)) (10,0)
Error DivMod zero denominator FailT "DivMod zero denominator"
>>>
pl @(DivMod (9 - Fst Id) (Last (Snd Id))) (10,[12,13])
Present (-1,12) (-1 `divMod` 13 = (-1,12)) PresentT (-1,12)
similar to quotRem
>>>
pz @(QuotRem (Fst Id) (Snd Id)) (10,3)
PresentT (3,1)
>>>
pz @(QuotRem (Fst Id) (Snd Id)) (10,-3)
PresentT (-3,1)
>>>
pz @(QuotRem (Fst Id) (Snd Id)) (-10,-3)
PresentT (3,-1)
>>>
pz @(QuotRem (Fst Id) (Snd Id)) (-10,3)
PresentT (-3,-1)
>>>
pz @(QuotRem (Fst Id) (Snd Id)) (10,0)
FailT "QuotRem zero denominator"
>>>
pl @(QuotRem (Negate Id) 7) 23
Present (-3,-2) (-23 `quotRem` 7 = (-3,-2)) PresentT (-3,-2)
>>>
pl @(QuotRem (Fst Id) (Snd Id)) (10,-3)
Present (-3,1) (10 `quotRem` -3 = (-3,1)) PresentT (-3,1)
similar to logBase
>>>
pz @(Fst Id `LogBase` Snd Id >> Truncate Int Id) (10,12345)
PresentT 4
similar to 'GHC.Real.(^)'
>>>
pz @(Fst Id ^ Snd Id) (10,4)
PresentT 10000
similar to 'GHC.Float.(**)'
>>>
pz @(Fst Id ** Snd Id) (10,4)
PresentT 10000.0
>>>
pz @'(Prime Id,Id ^ 3,(FromIntegral _ Id) ** (FromRational _ (1 % 2))) 4
PresentT (False,64,2.0)
rational numbers
creates a Rational
value
>>>
pz @(Id < 21 % 5) (-3.1)
TrueT
>>>
pz @(Id < 21 % 5) 4.5
FalseT
>>>
pz @(Fst Id % Snd Id) (13,2)
PresentT (13 % 2)
>>>
pz @(13 % Id) 0
FailT "(%) zero denominator"
>>>
pz @(4 % 3 + 5 % 7) "asfd"
PresentT (43 % 21)
>>>
pz @(4 -% 7 * 5 -% 3) "asfd"
PresentT (20 % 21)
>>>
pz @(Negate (14 % 3)) ()
PresentT ((-14) % 3)
>>>
pz @(14 % 3) ()
PresentT (14 % 3)
>>>
pz @(Negate (14 % 3) ==! FromIntegral _ (Negate 5)) ()
PresentT GT
>>>
pz @(14 -% 3 ==! 5 -% 1) "aa"
PresentT GT
>>>
pz @(Negate (14 % 3) ==! Negate 5 % 2) ()
PresentT LT
>>>
pz @(14 -% 3 * 5 -% 1) ()
PresentT (70 % 3)
>>>
pz @(14 % 3 ==! 5 % 1) ()
PresentT LT
>>>
pz @(15 % 3 / 4 % 2) ()
PresentT (5 % 2)
negate a ratio
>>>
pl @'[1 % 1 ,3 -% 2,3 -% 1] ()
Present [1 % 1,(-3) % 2,(-3) % 1] ('[1 % 1,(-3) % 2,(-3) % 1] (1 % 1) | ()) PresentT [1 % 1,(-3) % 2,(-3) % 1]
>>>
pl @('[1 % 1 ,Negate (33 % 7), 21 % 4,Signum (7 -% 5)] >> Map (Floor _ Id) Id) ()
Present [1,-5,5,-1] ((>>) [1,-5,5,-1] | {Map [1,-5,5,-1] | [1 % 1,(-33) % 7,21 % 4,(-1) % 1]}) PresentT [1,-5,5,-1]
>>>
pl @('[1 % 1 ,Negate (33 % 7), 21 % 4,Signum (7 -% 5)] >> Map (Ceiling _ Id) Id) ()
Present [1,-4,6,-1] ((>>) [1,-4,6,-1] | {Map [1,-4,6,-1] | [1 % 1,(-33) % 7,21 % 4,(-1) % 1]}) PresentT [1,-4,6,-1]
>>>
pl @('[1 % 1 ,Negate (33 % 7), 21 % 4,Signum (7 -% 5)] >> Map (Truncate _ Id) Id) ()
Present [1,-4,5,-1] ((>>) [1,-4,5,-1] | {Map [1,-4,5,-1] | [1 % 1,(-33) % 7,21 % 4,(-1) % 1]}) PresentT [1,-4,5,-1]
>>>
pl @(5 % 1 / 3 -% 1) 'x'
Present (-5) % 3 (5 % 1 / (-3) % 1 = (-5) % 3) PresentT ((-5) % 3)
>>>
pl @(5 -% 1 / Fst Id) (3,'x')
Present (-5) % 3 ((-5) % 1 / 3 % 1 = (-5) % 3) PresentT ((-5) % 3)
data ToRational p Source #
toRational
function
>>>
pz @(ToRational Id) 23.5
PresentT (47 % 2)
>>>
pl @((ToRational 123 &&& Id) >> Fst Id + Snd Id) 4.2
Present 636 % 5 ((>>) 636 % 5 | {123 % 1 + 21 % 5 = 636 % 5}) PresentT (636 % 5)
>>>
pl @(Fst Id >= Snd Id || Snd Id > 23 || 12 -% 5 <= ToRational (Fst Id)) (12,13)
True (False || True) TrueT
>>>
pl @(ToRational 14) ()
Present 14 % 1 (ToRational 14 % 1 | 14) PresentT (14 % 1)
>>>
pl @(ToRational 5 / ToRational 3) 'x'
Present 5 % 3 (5 % 1 / 3 % 1 = 5 % 3) PresentT (5 % 3)
Instances
(a ~ PP p x, Show a, Real a, P p x) => P (ToRational p :: Type) x Source # | |
Defined in Predicate.Data.Numeric type PP (ToRational p) x :: Type Source # eval :: MonadEval m => proxy (ToRational p) -> POpts -> x -> m (TT (PP (ToRational p) x)) Source # | |
type PP (ToRational p :: Type) x Source # | |
Defined in Predicate.Data.Numeric |
data FromRational (t :: Type) p Source #
fromRational
function where you need to provide the type 't' of the result
>>>
pz @(FromRational Rational Id) 23.5
PresentT (47 % 2)
>>>
pl @(FromRational Float (4 % 5)) ()
Present 0.8 (FromRational 0.8 | 4 % 5) PresentT 0.8
Instances
P (FromRationalT t p) x => P (FromRational t p :: Type) x Source # | |
Defined in Predicate.Data.Numeric type PP (FromRational t p) x :: Type Source # eval :: MonadEval m => proxy (FromRational t p) -> POpts -> x -> m (TT (PP (FromRational t p) x)) Source # | |
type PP (FromRational t p :: Type) x Source # | |
Defined in Predicate.Data.Numeric |
data FromRational' t r Source #
fromRational
function where you need to provide the type 't' of the result
>>>
pl @(FromRational' (Fst Id) (Snd Id)) (1::Float,2 % 5)
Present 0.4 (FromRational 0.4 | 2 % 5) PresentT 0.4
Instances
(P r a, PP r a ~ Rational, Show (PP t a), Fractional (PP t a)) => P (FromRational' t r :: Type) a Source # | |
Defined in Predicate.Data.Numeric type PP (FromRational' t r) a :: Type Source # eval :: MonadEval m => proxy (FromRational' t r) -> POpts -> a -> m (TT (PP (FromRational' t r) a)) Source # | |
type PP (FromRational' t r :: Type) a Source # | |
Defined in Predicate.Data.Numeric |
read / show expressions
data ReadBase (t :: Type) (n :: Nat) p Source #
Read a number using base 2 through a maximum of 36
>>>
pz @(ReadBase Int 16 Id) "00feD"
PresentT 4077
>>>
pz @(ReadBase Int 16 Id) "-ff"
PresentT (-255)
>>>
pz @(ReadBase Int 2 Id) "10010011"
PresentT 147
>>>
pz @(ReadBase Int 8 Id) "Abff"
FailT "invalid base 8"
>>>
pl @(ReadBase Int 16 Id >> GuardSimple (Id > 0xffff) >> ShowBase 16 Id) "12344"
Present "12344" ((>>) "12344" | {ShowBase(16) 12344 | 74564}) PresentT "12344"
>>>
:set -XBinaryLiterals
>>>
pz @(ReadBase Int 16 Id >> GuardSimple (Id > 0b10011111) >> ShowBase 16 Id) "7f"
FailT "(127 > 159)"
>>>
pl @(ReadBase Int 16 Id) "fFe0"
Present 65504 (ReadBase(Int,16) 65504 | "fFe0") PresentT 65504
>>>
pl @(ReadBase Int 16 Id) "-ff"
Present -255 (ReadBase(Int,16) -255 | "-ff") PresentT (-255)
>>>
pl @(ReadBase Int 16 Id) "ff"
Present 255 (ReadBase(Int,16) 255 | "ff") PresentT 255
>>>
pl @(ReadBase Int 22 Id) "zzz"
Error invalid base 22 (ReadBase(Int,22) as=zzz err=[]) FailT "invalid base 22"
>>>
pl @((ReadBase Int 16 Id &&& Id) >> First (ShowBase 16 Id)) "fFe0"
Present ("ffe0","fFe0") ((>>) ("ffe0","fFe0") | {(***) ("ffe0","fFe0") | (65504,"fFe0")}) PresentT ("ffe0","fFe0")
>>>
pl @(ReadBase Int 2 Id) "101111"
Present 47 (ReadBase(Int,2) 47 | "101111") PresentT 47
data ShowBase (n :: Nat) p Source #
Display a number at base 2 to 36, similar to showIntAtBase
but supports signed numbers
>>>
pz @(ShowBase 16 Id) 4077
PresentT "fed"
>>>
pz @(ShowBase 16 Id) (-255)
PresentT "-ff"
>>>
pz @(ShowBase 2 Id) 147
PresentT "10010011"
>>>
pz @(ShowBase 2 (Negate 147)) "whatever"
PresentT "-10010011"
>>>
pl @(ShowBase 16 Id) (-123)
Present "-7b" (ShowBase(16) -7b | -123) PresentT "-7b"
>>>
pl @(ShowBase 16 Id) 123
Present "7b" (ShowBase(16) 7b | 123) PresentT "7b"
>>>
pl @(ShowBase 16 Id) 65504
Present "ffe0" (ShowBase(16) ffe0 | 65504) PresentT "ffe0"