module Data.TypeLevel.Num.Ops
(
Succ, succ,
Pred, pred,
Add, (+),
Sub, (),
Mul, (*),
Div, div,
Mod, mod,
DivMod, divMod,
IsDivBy, isDivBy,
Mul10, mul10,
Div10, div10,
DivMod10, divMod10,
ExpBase, (^),
LogBase, logBase,
LogBaseF, logBaseF,
IsPowOf, isPowOf,
Exp10, exp10,
Log10, log10,
Trich, trich,
LT, EQ, GT,
(:==:), (:>:), (:<:), (:>=:), (:<=:),
(==) , (>) , (<) , (>=) , (<=),
Max, max,
Min, min,
GCD, gcd
) where
import Data.TypeLevel.Num.Reps
import Data.TypeLevel.Num.Sets
import Data.TypeLevel.Bool
import Prelude hiding
(succ, pred, (+), (), (*), div, mod, divMod, (^), logBase,
(==), (>), (<), (<), (>=), (<=), max, min, gcd, Bool)
class (Nat x, Pos y) => Succ x y | x -> y, y -> x
instance (Pos y, IsZero y yz, DivMod10 x xi xl, Succ' xi xl yi yl yz,
DivMod10 y yi yl)
=> Succ x y
class Succ' xh xl yh yl yz | xh xl -> yh yl yz, yh yl yz -> xh xl
class Failure t
data PredecessorOfZeroError t
instance Failure (PredecessorOfZeroError x) => Succ' (x,x) (x,x) D0 D0 True
instance Succ' xi D0 xi D1 False
instance Succ' xi D1 xi D2 False
instance Succ' xi D2 xi D3 False
instance Succ' xi D3 xi D4 False
instance Succ' xi D4 xi D5 False
instance Succ' xi D5 xi D6 False
instance Succ' xi D6 xi D7 False
instance Succ' xi D7 xi D8 False
instance Succ' xi D8 xi D9 False
instance Succ xi yi => Succ' xi D9 yi D0 False
succ :: Succ x y => x -> y
succ = undefined
class (Pos x, Nat y) => Pred x y | x -> y, y -> x
instance Succ x y => Pred y x
pred :: Pred x y => x -> y
pred = undefined
class (Nat x, Nat y, Nat z) => Add' x y z | x y -> z, z x -> y
instance Nat y => Add' D0 y y
instance Succ y z => Add' D1 y z
instance (Succ z z', Add' D1 y z) => Add' D2 y z'
instance (Succ z z', Add' D2 y z) => Add' D3 y z'
instance (Succ z z', Add' D3 y z) => Add' D4 y z'
instance (Succ z z', Add' D4 y z) => Add' D5 y z'
instance (Succ z z', Add' D5 y z) => Add' D6 y z'
instance (Succ z z', Add' D6 y z) => Add' D7 y z'
instance (Succ z z', Add' D7 y z) => Add' D8 y z'
instance (Succ z z', Add' D8 y z) => Add' D9 y z'
instance (Pos (xi :* xl), Nat z,
Add' xi yi zi, DivMod10 y yi yl, Add' xl (zi :* yl) z)
=> Add' (xi :* xl) y z
class (Add' x y z, Add' y x z) => Add x y z | x y -> z, z x -> y, z y -> x
instance (Add' x y z, Add' y x z) => Add x y z
(+) :: (Add x y z) => x -> y -> z
(+) = undefined
class Sub x y z | x y -> z, z x -> y, z y -> x
instance Add x y z => Sub z y x
() :: (Sub x y z) => x -> y -> z
() = undefined
infixl 6 +,
class (Nat x, Nat y, Nat z) => Mul x y z | x y -> z
instance Nat y => Mul D0 y D0
instance Nat y => Mul D1 y y
instance Add y y z => Mul D2 y z
instance (Add z y z', Mul D2 y z) => Mul D3 y z'
instance (Add z y z', Mul D3 y z) => Mul D4 y z'
instance (Add z y z', Mul D4 y z) => Mul D5 y z'
instance (Add z y z', Mul D5 y z) => Mul D6 y z'
instance (Add z y z', Mul D6 y z) => Mul D7 y z'
instance (Add z y z', Mul D7 y z) => Mul D8 y z'
instance (Add z y z', Mul D8 y z) => Mul D9 y z'
instance (Pos (xi :* xl), Nat y, Mul xi y z, Mul10 z z10, Mul xl y dy,
Add dy z10 z') => Mul (xi :* xl) y z'
(*) :: Mul x y z => x -> y -> z
(*) = undefined
infixl 7 *
class (Nat x, Pos y) => DivMod x y q r | x y -> q r
instance (Pos y, Trich x y cmp, DivMod' x y q r cmp) => DivMod x y q r
class (Nat x, Pos y) => DivMod' x y q r cmp | x y cmp -> q r,
q r cmp y -> x,
q r cmp x -> y
instance (Nat x, Pos y) => DivMod' x y D0 x LT
instance (Nat x, Pos y) => DivMod' x y D1 D0 EQ
instance (Nat x, Pos y, Sub x y x', Pred q q', DivMod x' y q' r)
=> DivMod' x y q r GT
divMod :: DivMod x y q r => x -> y -> (q,r)
divMod _ _ = (undefined, undefined)
class Div x y z | x y -> z, x z -> y, y z -> x
instance (DivMod x y q r) => Div x y q
div :: Div x y z => x -> y -> z
div = undefined
class Mod x y r | x y -> r
instance DivMod x y q r => Mod x y r
mod :: Mod x y r => x -> y -> r
mod = undefined
infixl 7 `div`, `mod`
class (Nat x, Nat q) => Mul10 x q | x -> q, q -> x
instance DivMod10 x q D0 => Mul10 q x
mul10 :: Mul10 x q => x -> q
mul10 = undefined
class (Nat i, Nat x) => DivMod10 x i l | i l -> x, x -> i l
instance DivMod10 D0 D0 D0
instance DivMod10 D1 D0 D1
instance DivMod10 D2 D0 D2
instance DivMod10 D3 D0 D3
instance DivMod10 D4 D0 D4
instance DivMod10 D5 D0 D5
instance DivMod10 D6 D0 D6
instance DivMod10 D7 D0 D7
instance DivMod10 D8 D0 D8
instance DivMod10 D9 D0 D9
instance (Nat (D1 :* l)) => DivMod10 (D1 :* l) D1 l
instance (Nat (D2 :* l)) => DivMod10 (D2 :* l) D2 l
instance (Nat (D3 :* l)) => DivMod10 (D3 :* l) D3 l
instance (Nat (D4 :* l)) => DivMod10 (D4 :* l) D4 l
instance (Nat (D5 :* l)) => DivMod10 (D5 :* l) D5 l
instance (Nat (D6 :* l)) => DivMod10 (D6 :* l) D6 l
instance (Nat (D7 :* l)) => DivMod10 (D7 :* l) D7 l
instance (Nat (D8 :* l)) => DivMod10 (D8 :* l) D8 l
instance (Nat (D9 :* l)) => DivMod10 (D9 :* l) D9 l
instance (Nat (x :* l), Nat ((x :* l) :* l')) =>
DivMod10 ((x :* l) :* l') (x :* l) l'
divMod10 :: DivMod10 x q r => x -> (q,r)
divMod10 _ = (undefined, undefined)
class (Nat x, Nat q) => Div10 x q | x -> q, q -> x
instance DivMod10 x q r => Div10 x q
div10 :: Div10 x q => x -> q
div10 = undefined
class (Pos d, Nat x) => IsDivBy d x
instance (DivMod x d q D0) => IsDivBy d x
isDivBy :: IsDivBy d x => d -> x
isDivBy = undefined
class (Nat b, Nat e, Nat r) => ExpBase b e r | b e -> r
instance Nat b => ExpBase b D0 D1
instance Nat b => ExpBase b D1 b
instance (Mul b b r) => ExpBase b D2 r
instance (Mul r b r', ExpBase b D2 r) => ExpBase b D3 r'
instance (Mul r b r', ExpBase b D3 r) => ExpBase b D4 r'
instance (Mul r b r', ExpBase b D4 r) => ExpBase b D5 r'
instance (Mul r b r', ExpBase b D5 r) => ExpBase b D6 r'
instance (Mul r b r', ExpBase b D6 r) => ExpBase b D7 r'
instance (Mul r b r', ExpBase b D7 r) => ExpBase b D8 r'
instance (Mul r b r', ExpBase b D8 r) => ExpBase b D9 r'
instance (Nat b, Pos (ei :* el), Nat r,
Mul b r r', Pred (ei :* el) e', ExpBase b e' r)
=> ExpBase b (ei :* el) r'
(^) :: ExpBase b e r => b -> e -> r
(^) = undefined
infixr 8 ^
class (Pos b, b :>=: D2, Pos x, Nat e) => LogBase b x e | b x -> e
instance LogBaseF b x e f => LogBase b x e
logBase :: LogBaseF b x e f => b -> x -> e
logBase = undefined
class (Pos b, b :>=: D2, Pos x, Nat e, Bool f)
=> LogBaseF b x e f | b x -> e f
instance (Trich x b cmp, LogBaseF' b x e f cmp) => LogBaseF b x e f
class (Pos b, b :>=: D2, Pos x, Nat e, Bool f)
=> LogBaseF' b x e f cmp | b x cmp -> e f
instance (Pos b, b :>=: D2, Pos x) => LogBaseF' b x D0 False LT
instance (Pos b, b :>=: D2) => LogBaseF' b b D1 True EQ
instance (Pos b, b :>=: D2, Pos x, DivMod x b q r, IsZero r rz, And rz f' f,
Pred e e', LogBaseF b q e' f') => LogBaseF' b x e f GT
logBaseF :: LogBaseF b x e f => b -> x -> (e,f)
logBaseF _ _ = (undefined, undefined)
class (Pos b, b :>=: D2, Pos x) => IsPowOf b x
instance (Trich x b cmp, IsPowOf' b x cmp) => IsPowOf b x
class (Pos b, b :>=: D2, Pos x) => IsPowOf' b x cmp
instance (Pos b, b :>=: D2) => IsPowOf' b b EQ
instance (Pos b, b :>=: D2, Pos x, DivMod x b q D0, IsPowOf b q)
=> IsPowOf' b x GT
isPowOf :: IsPowOf b x => b -> x -> ()
isPowOf = undefined
class (Nat x, Pos y) => Exp10 x y | x -> y, y -> x
instance Exp10 D0 D1
instance Exp10 D1 (D1 :* D0)
instance Exp10 D2 (D1 :* D0 :* D0)
instance Exp10 D3 (D1 :* D0 :* D0 :* D0)
instance Exp10 D4 (D1 :* D0 :* D0 :* D0 :* D0)
instance Exp10 D5 (D1 :* D0 :* D0 :* D0 :* D0 :* D0)
instance Exp10 D6 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
instance Exp10 D7 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
instance Exp10 D8 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
instance Exp10 D9 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
instance (Pred (xi :* xl) x',
Exp10 x' (y :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0))
=> Exp10 (xi :* xl)
(y :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
exp10 :: Exp10 x y => x -> y
exp10 = undefined
class (Pos x, Nat y) => Log10 x y | x -> y
instance Log10 D1 D0
instance Log10 D2 D0
instance Log10 D3 D0
instance Log10 D4 D0
instance Log10 D5 D0
instance Log10 D6 D0
instance Log10 D7 D0
instance Log10 D8 D0
instance Log10 D9 D0
instance (Pos (xi :* xl), Pred y y', Log10 xi y') => Log10 (xi :* xl) y
log10 :: Log10 x y => x -> y
log10 = undefined
data LT
data EQ
data GT
class (Nat x, Nat y) => Trich x y r | x y -> r
trich :: Trich x y r => z -> x -> r
trich = undefined
instance Trich D0 D0 EQ
instance Trich D0 D1 LT
instance Trich D0 D2 LT
instance Trich D0 D3 LT
instance Trich D0 D4 LT
instance Trich D0 D5 LT
instance Trich D0 D6 LT
instance Trich D0 D7 LT
instance Trich D0 D8 LT
instance Trich D0 D9 LT
instance Pos (yi :* yl) => Trich D0 (yi :* yl) LT
instance Pos (yi :* yl) => Trich (yi :* yl) D0 GT
instance Trich D1 D0 GT
instance Trich D1 D1 EQ
instance Trich D1 D2 LT
instance Trich D1 D3 LT
instance Trich D1 D4 LT
instance Trich D1 D5 LT
instance Trich D1 D6 LT
instance Trich D1 D7 LT
instance Trich D1 D8 LT
instance Trich D1 D9 LT
instance Pos (yi :* yl) => Trich D1 (yi :* yl) LT
instance Pos (yi :* yl) => Trich (yi :* yl) D1 GT
instance Trich D2 D0 GT
instance Trich D2 D1 GT
instance Trich D2 D2 EQ
instance Trich D2 D3 LT
instance Trich D2 D4 LT
instance Trich D2 D5 LT
instance Trich D2 D6 LT
instance Trich D2 D7 LT
instance Trich D2 D8 LT
instance Trich D2 D9 LT
instance Pos (yi :* yl) => Trich D2 (yi :* yl) LT
instance Pos (yi :* yl) => Trich (yi :* yl) D2 GT
instance Trich D3 D0 GT
instance Trich D3 D1 GT
instance Trich D3 D2 GT
instance Trich D3 D3 EQ
instance Trich D3 D4 LT
instance Trich D3 D5 LT
instance Trich D3 D6 LT
instance Trich D3 D7 LT
instance Trich D3 D8 LT
instance Trich D3 D9 LT
instance Pos (yi :* yl) => Trich D3 (yi :* yl) LT
instance Pos (yi :* yl) => Trich (yi :* yl) D3 GT
instance Trich D4 D0 GT
instance Trich D4 D1 GT
instance Trich D4 D2 GT
instance Trich D4 D3 GT
instance Trich D4 D4 EQ
instance Trich D4 D5 LT
instance Trich D4 D6 LT
instance Trich D4 D7 LT
instance Trich D4 D8 LT
instance Trich D4 D9 LT
instance Pos (yi :* yl) => Trich D4 (yi :* yl) LT
instance Pos (yi :* yl) => Trich (yi :* yl) D4 GT
instance Trich D5 D0 GT
instance Trich D5 D1 GT
instance Trich D5 D2 GT
instance Trich D5 D3 GT
instance Trich D5 D4 GT
instance Trich D5 D5 EQ
instance Trich D5 D6 LT
instance Trich D5 D7 LT
instance Trich D5 D8 LT
instance Trich D5 D9 LT
instance Pos (yi :* yl) => Trich D5 (yi :* yl) LT
instance Pos (yi :* yl) => Trich (yi :* yl) D5 GT
instance Trich D6 D0 GT
instance Trich D6 D1 GT
instance Trich D6 D2 GT
instance Trich D6 D3 GT
instance Trich D6 D4 GT
instance Trich D6 D5 GT
instance Trich D6 D6 EQ
instance Trich D6 D7 LT
instance Trich D6 D8 LT
instance Trich D6 D9 LT
instance Pos (yi :* yl) => Trich D6 (yi :* yl) LT
instance Pos (yi :* yl) => Trich (yi :* yl) D6 GT
instance Trich D7 D0 GT
instance Trich D7 D1 GT
instance Trich D7 D2 GT
instance Trich D7 D3 GT
instance Trich D7 D4 GT
instance Trich D7 D5 GT
instance Trich D7 D6 GT
instance Trich D7 D7 EQ
instance Trich D7 D8 LT
instance Trich D7 D9 LT
instance Pos (yi :* yl) => Trich D7 (yi :* yl) LT
instance Pos (yi :* yl) => Trich (yi :* yl) D7 GT
instance Trich D8 D0 GT
instance Trich D8 D1 GT
instance Trich D8 D2 GT
instance Trich D8 D3 GT
instance Trich D8 D4 GT
instance Trich D8 D5 GT
instance Trich D8 D6 GT
instance Trich D8 D7 GT
instance Trich D8 D8 EQ
instance Trich D8 D9 LT
instance Pos (yi :* yl) => Trich D8 (yi :* yl) LT
instance Pos (yi :* yl) => Trich (yi :* yl) D8 GT
instance Trich D9 D0 GT
instance Trich D9 D1 GT
instance Trich D9 D2 GT
instance Trich D9 D3 GT
instance Trich D9 D4 GT
instance Trich D9 D5 GT
instance Trich D9 D6 GT
instance Trich D9 D7 GT
instance Trich D9 D8 GT
instance Trich D9 D9 EQ
instance Pos (yi :* yl) => Trich D9 (yi :* yl) LT
instance Pos (yi :* yl) => Trich (yi :* yl) D9 GT
instance (Pos (xi :* xl), Pos (yi :* yl), Trich xl yl rl, Trich xi yi ri,
CS ri rl r) => Trich (xi :* xl) (yi :* yl) r
class CS r1 r2 r3 | r1 r2 -> r3
instance CS EQ r r
instance CS GT r GT
instance CS LT r LT
class x :==: y
instance (Trich x y EQ) => (:==:) x y
(==) :: (x :==: y) => x -> y -> ()
(==) = undefined
class x :>: y
instance (Trich x y GT) => (:>:) x y
(>) :: (x :>: y) => x -> y -> ()
(>) = undefined
class x :<: y
instance (Trich x y LT) => (:<:) x y
(<) :: (x :<: y) => x -> y -> ()
(<) = undefined
class x :>=: y
instance (Succ x x', Trich x' y GT) => (:>=:) x y
(>=) :: (x :>=: y) => x -> y -> ()
(>=) = undefined
class x :<=: y
instance (Succ x' x, Trich x' y LT) => (:<=:) x y
(<=) :: (x :<=: y) => x -> y -> ()
(<=) = undefined
infix 4 <,<=,>=,>,==
class Max' x y b r | x y b -> r
instance Max' x y LT y
instance Max' x y EQ y
instance Max' x y GT x
class Max x y z | x y -> z
instance (Max' x y b z, Trich x y b) => Max x y z
max :: Max x y z => x -> y -> z
max = undefined
class Min x y z | x y -> z
instance (Max' y x b z, Trich x y b) => Min x y z
min :: Min x y z => x -> y -> z
min = undefined
class (Nat x, Nat y, Nat gcd) => GCD x y gcd | x y -> gcd
instance (Nat x, Nat y, Trich x y cmp, IsZero y yz, GCD' x y yz cmp gcd)
=> GCD x y gcd
class (Nat x, Nat y, Nat gcd) => GCD' x y yz cmp gcd | x y yz cmp -> gcd
instance Nat x => GCD' x D0 True cmp D0
instance (Nat x, Nat y, GCD y x gcd) => GCD' x y False LT gcd
instance Nat x => GCD' x x False EQ x
instance (Nat x, Nat y, Sub x y x', GCD x' y gcd) => GCD' x y False GT gcd
gcd :: GCD x y z => x -> y -> z
gcd = undefined
class IsZero x r | x -> r
instance IsZero D0 True
instance IsZero D1 False
instance IsZero D2 False
instance IsZero D3 False
instance IsZero D4 False
instance IsZero D5 False
instance IsZero D6 False
instance IsZero D7 False
instance IsZero D8 False
instance IsZero D9 False
instance Pos x => IsZero (x :* d) False