{-# OPTIONS -Wall #-}
{-# OPTIONS -Wno-compat #-}
{-# OPTIONS -Wincomplete-record-updates #-}
{-# OPTIONS -Wincomplete-uni-patterns #-}
{-# OPTIONS -Wredundant-constraints #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoOverloadedLists #-}
{-# LANGUAGE NoStarIsType #-}
module Predicate.Data.Numeric (
type (+)
, type (-)
, type (*)
, type (/)
, Negate
, Abs
, Signum
, FromInteger
, FromInteger'
, FromIntegral
, FromIntegral'
, Truncate
, Truncate'
, Ceiling
, Ceiling'
, Floor
, Floor'
, Even
, Odd
, Div
, Mod
, DivMod
, QuotRem
, Quot
, Rem
, LogBase
, type (^)
, type (**)
, type (%)
, type (-%)
, ToRational
, FromRational
, FromRational'
, ReadBase
, ReadBase'
, ShowBase
) where
import Predicate.Core
import Predicate.Util
import Predicate.Data.Ordering (type (==))
import GHC.TypeLits (Nat,KnownNat)
import qualified GHC.TypeLits as GL
import Data.List
import Data.Proxy
import Data.Typeable
import Data.Kind (Type)
import Data.Maybe
import qualified Numeric
import Data.Char
import Data.Ratio
import GHC.Real (Ratio((:%)))
data FromInteger' t n
instance (Num (PP t a)
, Integral (PP n a)
, P n a
, Show (PP t a)
) => P (FromInteger' t n) a where
type PP (FromInteger' t n) a = PP t a
eval _ opts a = do
let msg0 = "FromInteger"
nn <- eval (Proxy @n) opts a
pure $ case getValueLR opts msg0 nn [] of
Left e -> e
Right n ->
let b = fromInteger (fromIntegral n)
in mkNode opts (PresentT b) (msg0 <> " " <> showL opts b) [hh nn]
data FromInteger (t :: Type) p
type FromIntegerT (t :: Type) p = FromInteger' (Hole t) p
instance P (FromIntegerT t p) x => P (FromInteger t p) x where
type PP (FromInteger t p) x = PP (FromIntegerT t p) x
eval _ = eval (Proxy @(FromIntegerT t p))
data FromIntegral' t n
instance (Num (PP t a)
, Integral (PP n a)
, P n a
, Show (PP t a)
, Show (PP n a)
) => P (FromIntegral' t n) a where
type PP (FromIntegral' t n) a = PP t a
eval _ opts a = do
let msg0 = "FromIntegral"
nn <- eval (Proxy @n) opts a
pure $ case getValueLR opts msg0 nn [] of
Left e -> e
Right n ->
let b = fromIntegral n
in mkNode opts (PresentT b) (show01 opts msg0 b n) [hh nn]
data FromIntegral (t :: Type) p
type FromIntegralT (t :: Type) p = FromIntegral' (Hole t) p
instance P (FromIntegralT t p) x => P (FromIntegral t p) x where
type PP (FromIntegral t p) x = PP (FromIntegralT t p) x
eval _ = eval (Proxy @(FromIntegralT t p))
data ToRational p
instance (a ~ PP p x
, Show a
, Real a
, P p x)
=> P (ToRational p) x where
type PP (ToRational p) x = Rational
eval _ opts x = do
let msg0 = "ToRational"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right a ->
let r = toRational a
in mkNode opts (PresentT r) (show01 opts msg0 r a) [hh pp]
data FromRational' t r
instance (P r a
, PP r a ~ Rational
, Show (PP t a)
, Fractional (PP t a)
) => P (FromRational' t r) a where
type PP (FromRational' t r) a = PP t a
eval _ opts a = do
let msg0 = "FromRational"
rr <- eval (Proxy @r) opts a
pure $ case getValueLR opts msg0 rr [] of
Left e -> e
Right r ->
let b = fromRational @(PP t a) r
in mkNode opts (PresentT b) (show01 opts msg0 b r) [hh rr]
data FromRational (t :: Type) p
type FromRationalT (t :: Type) p = FromRational' (Hole t) p
instance P (FromRationalT t p) x => P (FromRational t p) x where
type PP (FromRational t p) x = PP (FromRationalT t p) x
eval _ = eval (Proxy @(FromRationalT t p))
data Truncate' t p
instance (Show (PP p x)
, P p x
, Show (PP t x)
, RealFrac (PP p x)
, Integral (PP t x)
) => P (Truncate' t p) x where
type PP (Truncate' t p) x = PP t x
eval _ opts x = do
let msg0 = "Truncate"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = truncate p
in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
data Truncate (t :: Type) p
type TruncateT (t :: Type) p = Truncate' (Hole t) p
instance P (TruncateT t p) x => P (Truncate t p) x where
type PP (Truncate t p) x = PP (TruncateT t p) x
eval _ = eval (Proxy @(TruncateT t p))
data Ceiling' t p
instance (Show (PP p x)
, P p x
, Show (PP t x)
, RealFrac (PP p x)
, Integral (PP t x)
) => P (Ceiling' t p) x where
type PP (Ceiling' t p) x = PP t x
eval _ opts x = do
let msg0 = "Ceiling"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = ceiling p
in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
data Ceiling (t :: Type) p
type CeilingT (t :: Type) p = Ceiling' (Hole t) p
instance P (CeilingT t p) x => P (Ceiling t p) x where
type PP (Ceiling t p) x = PP (CeilingT t p) x
eval _ = eval (Proxy @(CeilingT t p))
data Floor' t p
instance (Show (PP p x)
, P p x
, Show (PP t x)
, RealFrac (PP p x)
, Integral (PP t x)
) => P (Floor' t p) x where
type PP (Floor' t p) x = PP t x
eval _ opts x = do
let msg0 = "Floor"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let b = floor p
in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
data Floor (t :: Type) p
type FloorT (t :: Type) p = Floor' (Hole t) p
instance P (FloorT t p) x => P (Floor t p) x where
type PP (Floor t p) x = PP (FloorT t p) x
eval _ = eval (Proxy @(FloorT t p))
data BinOp = BMult | BSub | BAdd deriving (Show,Eq)
data p + q
infixl 6 +
type AddT p q = Bin 'BAdd p q
instance P (AddT p q) x => P (p + q) x where
type PP (p + q) x = PP (AddT p q) x
eval _ = eval (Proxy @(AddT p q))
data p - q
infixl 6 -
type SubT p q = Bin 'BSub p q
instance P (SubT p q) x => P (p - q) x where
type PP (p - q) x = PP (SubT p q) x
eval _ = eval (Proxy @(SubT p q))
data p * q
infixl 7 *
type MultT p q = Bin 'BMult p q
instance P (MultT p q) x => P (p * q) x where
type PP (p * q) x = PP (MultT p q) x
eval _ = eval (Proxy @(MultT p q))
data p ^ q
infixr 8 ^
instance (P p a
, P q a
, Show (PP p a)
, Show (PP q a)
, Num (PP p a)
, Integral (PP q a)
) => P (p ^ q) a where
type PP (p ^ q) a = PP p a
eval _ opts a = do
let msg0 = "Pow"
pp <- eval (Proxy @p) opts a
case getValueLR opts msg0 pp [] of
Left e -> pure e
Right p -> do
qq <- eval (Proxy @q) opts a
pure $ case getValueLR opts msg0 qq [hh pp] of
Left e -> e
Right q ->
let hhs = [hh pp, hh qq]
in if q < 0 then mkNode opts (FailT (msg0 <> " negative exponent")) "" hhs
else let d = p ^ q
in mkNode opts (PresentT d) (showL opts p <> " ^ " <> showL opts q <> " = " <> showL opts d) hhs
data p ** q
infixr 8 **
instance (PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Floating (PP p a)
, Ord (PP q a)
) => P (p ** q) a where
type PP (p ** q) a = PP p a
eval _ opts a = do
let msg0 = "Exp"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in if q < 0 then mkNode opts (FailT (msg0 <> " negative exponent")) "" hhs
else if p == 0 && q == 0 then mkNode opts (FailT (msg0 <> " zero/zero")) "" hhs
else let d = p ** q
in mkNode opts (PresentT d) (showL opts p <> " ** " <> showL opts q <> " = " <> showL opts d) hhs
data LogBase p q
instance (PP p a ~ PP q a
, P p a
, P q a
, Show (PP q a)
, Floating (PP q a)
, Ord (PP p a)
) => P (LogBase p q) a where
type PP (LogBase p q) a = PP p a
eval _ opts a = do
let msg0 = "LogBase"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in if p <= 0 then mkNode opts (FailT (msg0 <> " non-positive base")) "" hhs
else let d = logBase p q
in mkNode opts (PresentT d) (msg0 <> " " <> showL opts p <> " " <> showL opts q <> " = " <> showL opts d) hhs
class GetBinOp (k :: BinOp) where
getBinOp :: (Num a, a ~ b) => (String, a -> b -> a)
instance GetBinOp 'BMult where
getBinOp = ("*",(*))
instance GetBinOp 'BSub where
getBinOp = ("-",(-))
instance GetBinOp 'BAdd where
getBinOp = ("+",(+))
data Bin (op :: BinOp) p q
instance (GetBinOp op
, PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Num (PP p a)
) => P (Bin op p q) a where
type PP (Bin op p q) a = PP p a
eval _ opts a = do
let (s,f) = getBinOp @op
lr <- runPQ s (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let d = p `f` q
in mkNode opts (PresentT d) (showL opts p <> " " <> s <> " " <> showL opts q <> " = " <> showL opts d) [hh pp, hh qq]
data p / q
infixl 7 /
instance (PP p a ~ PP q a
, Eq (PP q a)
, P p a
, P q a
, Show (PP p a)
, Fractional (PP p a)
) => P (p / q) a where
type PP (p / q) a = PP p a
eval _ opts a = do
let msg0 = "(/)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq)
| q == 0 -> let msg1 = msg0 <> " zero denominator"
in mkNode opts (FailT msg1) "" [hh pp, hh qq]
| otherwise ->
let d = p / q
in mkNode opts (PresentT d) (showL opts p <> " / " <> showL opts q <> " = " <> showL opts d) [hh pp, hh qq]
data p % q
infixl 8 %
instance (Integral (PP p x)
, Integral (PP q x)
, Eq (PP q x)
, P p x
, P q x
, Show (PP p x)
, Show (PP q x)
) => P (p % q) x where
type PP (p % q) x = Rational
eval _ opts x = do
let msg0 = "(%)"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq)
| q == 0 -> let msg1 = msg0 <> " zero denominator"
in mkNode opts (FailT msg1) "" [hh pp, hh qq]
| otherwise ->
let z@(p1,q1) = (fromIntegral p, fromIntegral q)
d@(dn :% dd) = uncurry (%) z
zz = if dn == p1 && dd == q1 then ""
else litVerbose opts " | " (show p <> " % " <> show q)
in mkNode opts (PresentT d) (showL opts d <> zz) [hh pp, hh qq]
data p -% q
infixl 8 -%
type NegateRatioT p q = Negate (p % q)
instance P (NegateRatioT p q) x => P (p -% q) x where
type PP (p -% q) x = PP (NegateRatioT p q) x
eval _ = eval (Proxy @(NegateRatioT p q))
data Negate p
instance ( Show (PP p x)
, Num (PP p x)
, P p x
) => P (Negate p) x where
type PP (Negate p) x = PP p x
eval _ opts x = do
let msg0 = "Negate"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = negate p
in mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
data Abs p
instance ( Show (PP p x)
, Num (PP p x)
, P p x
) => P (Abs p) x where
type PP (Abs p) x = PP p x
eval _ opts x = do
let msg0 = "Abs"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = abs p
in mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
data Div p q
instance (PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Integral (PP p a)
) => P (Div p q) a where
type PP (Div p q) a = PP p a
eval _ opts a = do
let msg0 = "Div"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in case q of
0 -> mkNode opts (FailT (msg0 <> " zero denominator")) "" hhs
_ -> let d = p `div` q
in mkNode opts (PresentT d) (showL opts p <> " `div` " <> showL opts q <> " = " <> showL opts d) hhs
data Mod p q
instance (PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Integral (PP p a)
) => P (Mod p q) a where
type PP (Mod p q) a = PP p a
eval _ opts a = do
let msg0 = "Mod"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in case q of
0 -> mkNode opts (FailT (msg0 <> " zero denominator")) "" hhs
_ -> let d = p `mod` q
in mkNode opts (PresentT d) (showL opts p <> " `mod` " <> showL opts q <> " = " <> showL opts d) hhs
data DivMod p q
instance (PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Integral (PP p a)
) => P (DivMod p q) a where
type PP (DivMod p q) a = (PP p a, PP p a)
eval _ opts a = do
let msg0 = "DivMod"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in case q of
0 -> mkNode opts (FailT (msg0 <> " zero denominator")) "" hhs
_ -> let d = p `divMod` q
in mkNode opts (PresentT d) (showL opts p <> " `divMod` " <> showL opts q <> " = " <> showL opts d) hhs
data QuotRem p q
instance (PP p a ~ PP q a
, P p a
, P q a
, Show (PP p a)
, Integral (PP p a)
) => P (QuotRem p q) a where
type PP (QuotRem p q) a = (PP p a, PP p a)
eval _ opts a = do
let msg0 = "QuotRem"
lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
pure $ case lr of
Left e -> e
Right (p,q,pp,qq) ->
let hhs = [hh pp, hh qq]
in case q of
0 -> mkNode opts (FailT (msg0 <> " zero denominator")) "" hhs
_ -> let d = p `quotRem` q
in mkNode opts (PresentT d) (showL opts p <> " `quotRem` " <> showL opts q <> " = " <> showL opts d) hhs
data Quot p q
type QuotT p q = Fst (QuotRem p q)
instance P (QuotT p q) x => P (Quot p q) x where
type PP (Quot p q) x = PP (QuotT p q) x
eval _ = eval (Proxy @(QuotT p q))
data Rem p q
type RemT p q = Snd (QuotRem p q)
instance P (RemT p q) x => P (Rem p q) x where
type PP (Rem p q) x = PP (RemT p q) x
eval _ = eval (Proxy @(RemT p q))
data Even
type EvenT = Mod I 2 == 0
instance P EvenT x => P Even x where
type PP Even x = Bool
eval _ = evalBool (Proxy @EvenT)
data Odd
type OddT = Mod I 2 == 1
instance P OddT x => P Odd x where
type PP Odd x = Bool
eval _ = evalBool (Proxy @OddT)
data Signum p
instance ( Show (PP p x)
, Num (PP p x)
, P p x
) => P (Signum p) x where
type PP (Signum p) x = PP p x
eval _ opts x = do
let msg0 = "Signum"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let d = signum p
in mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
data ReadBase' t (n :: Nat) p
instance (Typeable (PP t x)
, ZwischenT 2 36 n
, Show (PP t x)
, Num (PP t x)
, KnownNat n
, PP p x ~ String
, P p x
) => P (ReadBase' t n p) x where
type PP (ReadBase' t n p) x = PP t x
eval _ opts x = do
let n = nat @n
xs = getValidBase n
msg0 = "ReadBase(" <> t <> "," <> show n <> ")"
t = showT @(PP t x)
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let (ff,p1) = case p of
'-':q -> (negate,q)
_ -> (id,p)
in case Numeric.readInt (fromIntegral n)
((`elem` xs) . toLower)
(fromJust . (`elemIndex` xs) . toLower)
p1 of
[(b,"")] -> mkNode opts (PresentT (ff b)) (msg0 <> " " <> showL opts (ff b) <> showVerbose opts " | " p) [hh pp]
o -> mkNode opts (FailT ("invalid base " <> show n)) (msg0 <> " as=" <> p <> " err=" <> showL opts o) [hh pp]
data ReadBase (t :: Type) (n :: Nat) p
type ReadBaseT (t :: Type) (n :: Nat) p = ReadBase' (Hole t) n p
instance P (ReadBaseT t n p) x => P (ReadBase t n p) x where
type PP (ReadBase t n p) x = PP (ReadBaseT t n p) x
eval _ = eval (Proxy @(ReadBaseT t n p))
getValidBase :: Int -> String
getValidBase n =
let xs = ['0'..'9'] <> ['a'..'z']
len = length xs
in if n > len || n < 2 then errorInProgram $ "getValidBase: oops invalid base valid is 2 thru " ++ show len ++ " found " ++ show n
else take n xs
data ShowBase (n :: Nat) p
instance (PP p x ~ a
, P p x
, Show a
, 2 GL.<= n
, n GL.<= 36
, KnownNat n
, Integral a
) => P (ShowBase n p) x where
type PP (ShowBase n p) x = String
eval _ opts x = do
let n = nat @n
xs = getValidBase n
msg0 = "ShowBase(" <> show n <> ")"
pp <- eval (Proxy @p) opts x
pure $ case getValueLR opts msg0 pp [] of
Left e -> e
Right p ->
let (ff,a') = if p < 0 then (('-':), abs p) else (id,p)
b = Numeric.showIntAtBase (fromIntegral n) (xs !!) a' ""
in mkNode opts (PresentT (ff b)) (msg0 <> " " <> litL opts (ff b) <> showVerbose opts " | " p) [hh pp]