module Data.TypeLevel.Num.Ops
(
Succ, succ,
Pred, pred,
Add, (+),
Sub, (),
Mul, (*),
Div, div,
Mod, mod,
IsDivBy, isDivBy,
Mul10, mul10,
Div10, div10,
DivMod10, divMod10,
ExpBase, (^),
Exp10, exp10,
Log10, log10,
Trich, trich,
LT, EQ, GT,
OrderingEq, NatEq,
(:>:), (:<:), (:>=:), (:<=:),
(>) , (<) , (>=) , (<=),
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)
type family Succ n
type instance Succ D0 = D1
type instance Succ D1 = D2
type instance Succ D2 = D3
type instance Succ D3 = D4
type instance Succ D4 = D5
type instance Succ D5 = D6
type instance Succ D6 = D7
type instance Succ D7 = D8
type instance Succ D8 = D9
type instance Succ D9 = (D1 :* D0)
type instance Succ (x:*D0) = (x:*D1)
type instance Succ (x:*D1) = (x:*D2)
type instance Succ (x:*D2) = (x:*D3)
type instance Succ (x:*D3) = (x:*D4)
type instance Succ (x:*D4) = (x:*D5)
type instance Succ (x:*D5) = (x:*D6)
type instance Succ (x:*D6) = (x:*D7)
type instance Succ (x:*D7) = (x:*D8)
type instance Succ (x:*D8) = (x:*D9)
type instance Succ (x:*D9) = (Succ x:*D0)
succ :: x -> Succ x
succ = undefined
type family Pred n
type instance Pred D1 = D0
type instance Pred D2 = D1
type instance Pred D3 = D2
type instance Pred D4 = D3
type instance Pred D5 = D4
type instance Pred D6 = D5
type instance Pred D7 = D6
type instance Pred D8 = D7
type instance Pred D9 = D8
type instance Pred (D1:*D0) = D9
type instance Pred (D2:*D0) = (D1:*D9)
type instance Pred (D3:*D0) = (D2:*D9)
type instance Pred (D4:*D0) = (D3:*D9)
type instance Pred (D5:*D0) = (D4:*D9)
type instance Pred (D6:*D0) = (D5:*D9)
type instance Pred (D7:*D0) = (D6:*D9)
type instance Pred (D8:*D0) = (D7:*D9)
type instance Pred (D9:*D0) = (D8:*D9)
type instance Pred (xd:*xm:*D0) = Pred(xd:*xm):*D9
type instance Pred (xd:*D1) = (xd:*D0)
type instance Pred (xd:*D2) = (xd:*D1)
type instance Pred (xd:*D3) = (xd:*D2)
type instance Pred (xd:*D4) = (xd:*D3)
type instance Pred (xd:*D5) = (xd:*D4)
type instance Pred (xd:*D6) = (xd:*D5)
type instance Pred (xd:*D7) = (xd:*D6)
type instance Pred (xd:*D8) = (xd:*D7)
type instance Pred (xd:*D9) = (xd:*D8)
pred :: x -> Pred x
pred = undefined
type family Div10 m
type instance Div10 D0 = D0
type instance Div10 D1 = D0
type instance Div10 D2 = D0
type instance Div10 D3 = D0
type instance Div10 D4 = D0
type instance Div10 D5 = D0
type instance Div10 D6 = D0
type instance Div10 D7 = D0
type instance Div10 D8 = D0
type instance Div10 D9 = D0
type instance Div10 (x:*D0) = x
type instance Div10 (x:*D1) = x
type instance Div10 (x:*D2) = x
type instance Div10 (x:*D3) = x
type instance Div10 (x:*D4) = x
type instance Div10 (x:*D5) = x
type instance Div10 (x:*D6) = x
type instance Div10 (x:*D7) = x
type instance Div10 (x:*D8) = x
type instance Div10 (x:*D9) = x
div10 :: x -> Div10 x
div10 = undefined
type family Mod10 n
type instance Mod10 D0 = D0
type instance Mod10 D1 = D1
type instance Mod10 D2 = D2
type instance Mod10 D3 = D3
type instance Mod10 D4 = D4
type instance Mod10 D5 = D5
type instance Mod10 D6 = D6
type instance Mod10 D7 = D7
type instance Mod10 D8 = D8
type instance Mod10 D9 = D9
type instance Mod10 (xd:*xm) = xm
mod10 :: x -> Mod10 x
mod10 = undefined
type family DivMod10 n
type instance DivMod10 n = (Div10 n, Mod10 n)
type family Add m n :: *
type instance Add D0 x = x
type instance Add D1 x = (Succ x)
type instance Add D2 x = Add D1 (Succ x)
type instance Add D3 x = Add D2 (Succ x)
type instance Add D4 x = Add D3 (Succ x)
type instance Add D5 x = Add D4 (Succ x)
type instance Add D6 x = Add D5 (Succ x)
type instance Add D7 x = Add D6 (Succ x)
type instance Add D8 x = Add D7 (Succ x)
type instance Add D9 x = Add D8 (Succ x)
type instance Add (xd :* xm) y = Add xm ((Add xd (Div10 y)) :* (Mod10 y))
(+) :: x -> y -> Add x y
(+) = undefined
type family Sub x y
type instance Sub x D0 = x
type instance Sub x D1 = (Pred x)
type instance Sub x D2 = Sub (Pred x) D1
type instance Sub x D3 = Sub (Pred x) D2
type instance Sub x D4 = Sub (Pred x) D3
type instance Sub x D5 = Sub (Pred x) D4
type instance Sub x D6 = Sub (Pred x) D5
type instance Sub x D7 = Sub (Pred x) D6
type instance Sub x D8 = Sub (Pred x) D7
type instance Sub x D9 = Sub (Pred x) D8
type instance Sub x (xd :* xm) = Sub (Pred x) (Pred (xd:*xm))
() :: x -> y -> Sub x y
() = undefined
type family Mul m n
type instance Mul D0 y = D0
type instance Mul D1 y = y
type instance Mul D2 y = Add y y
type instance Mul D3 y = Add y (Mul D2 y)
type instance Mul D4 y = Add y (Mul D3 y)
type instance Mul D5 y = Add y (Mul D4 y)
type instance Mul D6 y = Add y (Mul D5 y)
type instance Mul D7 y = Add y (Mul D6 y)
type instance Mul D8 y = Add y (Mul D7 y)
type instance Mul D9 y = Add y (Mul D8 y)
type instance Mul (xd :* xm) y = Add (Mul xm y) ((Mul xd y) :* D0)
(*) :: x -> y -> Mul x y
(*) = undefined
type family Div' x y x_gt_y
type instance Div' x y False = D0
type instance Div' x y True = Succ (Div' (Sub x y) y ((Sub x y) :>=: y))
type family Div x y
type instance Div x y = Div' x y (Trich x y)
type family Mod' x y x_gt_y
type instance Mod' x y False = x
type instance Mod' x y True = Mod' (Sub x y) y ((Sub x y) :>=: y)
type family Mod x y
type instance Mod x y = Mod' x y (x :>=: y)
divMod :: x -> y -> (Div x y, Mod x y)
divMod _ _ = (undefined)
div :: x -> y -> Div x y
div = undefined
mod :: x -> y -> Mod x y
mod = undefined
type family Mul10 n
type instance Mul10 x = (x :* D0)
mul10 :: x -> Mul10 x
mul10 = undefined
divMod10 :: x -> (Div10 x, Mod10 x)
divMod10 _ = (undefined, undefined)
class (Pos d, Nat x) => IsDivBy d x
instance (Pos d, Nat x, Mod x d ~ D0) => IsDivBy d x
isDivBy :: IsDivBy d x => d -> x -> ()
isDivBy _ _ = ()
type family ExpBase b e
type instance ExpBase b D0 = D1
type instance ExpBase b D1 = b
type instance ExpBase b D2 = (Mul b b)
type instance ExpBase b D3 = (Mul b (ExpBase b D2))
type instance ExpBase b D4 = (Mul b (ExpBase b D3))
type instance ExpBase b D5 = (Mul b (ExpBase b D4))
type instance ExpBase b D6 = (Mul b (ExpBase b D5))
type instance ExpBase b D7 = (Mul b (ExpBase b D6))
type instance ExpBase b D8 = (Mul b (ExpBase b D7))
type instance ExpBase b D9 = (Mul b (ExpBase b D8))
type instance ExpBase b (ei :* el) = Mul b (ExpBase b (Pred (ei:* el)))
(^) :: b -> e -> ExpBase b e
(^) = undefined
type family Exp10 x
type instance Exp10 D0 = D1
type instance Exp10 D1 = (D1 :* D0)
type instance Exp10 D2 = (D1 :* D0 :* D0)
type instance Exp10 D3 = (D1 :* D0 :* D0 :* D0)
type instance Exp10 D4 = (D1 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 D5 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 D6 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 D7 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 D8 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 D9 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 (xi :* xl) = (Exp10 (Pred (xi:*xl)) :* D0)
exp10 :: x -> Exp10 x
exp10 = undefined
type family Log10 x
type instance Log10 D1 = D0
type instance Log10 D2 = D0
type instance Log10 D3 = D0
type instance Log10 D4 = D0
type instance Log10 D5 = D0
type instance Log10 D6 = D0
type instance Log10 D7 = D0
type instance Log10 D8 = D0
type instance Log10 D9 = D0
type instance Log10 (xi :* xl) = Pred (Log10 xi)
log10 :: x -> Log10 x
log10 = undefined
---}
data LT
data EQ
data GT
type family OrderingEq o1 o2
type instance OrderingEq LT LT = True
type instance OrderingEq LT EQ = False
type instance OrderingEq LT GT = False
type instance OrderingEq EQ EQ = True
type instance OrderingEq EQ LT = False
type instance OrderingEq EQ GT = False
type instance OrderingEq GT GT = True
type instance OrderingEq GT LT = False
type instance OrderingEq GT EQ = False
type family Trich x y
trich :: x -> y -> Trich x y
trich = undefined
type instance Trich D0 D0 = EQ
type instance Trich D0 D1 = LT
type instance Trich D0 D2 = LT
type instance Trich D0 D3 = LT
type instance Trich D0 D4 = LT
type instance Trich D0 D5 = LT
type instance Trich D0 D6 = LT
type instance Trich D0 D7 = LT
type instance Trich D0 D8 = LT
type instance Trich D0 D9 = LT
type instance Trich D0 (yi :* yl) = LT
type instance Trich (yi :* yl) D0 = GT
type instance Trich D1 D0 = GT
type instance Trich D1 D1 = EQ
type instance Trich D1 D2 = LT
type instance Trich D1 D3 = LT
type instance Trich D1 D4 = LT
type instance Trich D1 D5 = LT
type instance Trich D1 D6 = LT
type instance Trich D1 D7 = LT
type instance Trich D1 D8 = LT
type instance Trich D1 D9 = LT
type instance Trich D1 (yi :* yl) = LT
type instance Trich (yi :* yl) D1 = GT
type instance Trich D2 D0 = GT
type instance Trich D2 D1 = GT
type instance Trich D2 D2 = EQ
type instance Trich D2 D3 = LT
type instance Trich D2 D4 = LT
type instance Trich D2 D5 = LT
type instance Trich D2 D6 = LT
type instance Trich D2 D7 = LT
type instance Trich D2 D8 = LT
type instance Trich D2 D9 = LT
type instance Trich D2 (yi :* yl) = LT
type instance Trich (yi :* yl) D2 = GT
type instance Trich D3 D0 = GT
type instance Trich D3 D1 = GT
type instance Trich D3 D2 = GT
type instance Trich D3 D3 = EQ
type instance Trich D3 D4 = LT
type instance Trich D3 D5 = LT
type instance Trich D3 D6 = LT
type instance Trich D3 D7 = LT
type instance Trich D3 D8 = LT
type instance Trich D3 D9 = LT
type instance Trich D3 (yi :* yl) = LT
type instance Trich (yi :* yl) D3 = GT
type instance Trich D4 D0 = GT
type instance Trich D4 D1 = GT
type instance Trich D4 D2 = GT
type instance Trich D4 D3 = GT
type instance Trich D4 D4 = EQ
type instance Trich D4 D5 = LT
type instance Trich D4 D6 = LT
type instance Trich D4 D7 = LT
type instance Trich D4 D8 = LT
type instance Trich D4 D9 = LT
type instance Trich D4 (yi :* yl) = LT
type instance Trich (yi :* yl) D4 = GT
type instance Trich D5 D0 = GT
type instance Trich D5 D1 = GT
type instance Trich D5 D2 = GT
type instance Trich D5 D3 = GT
type instance Trich D5 D4 = GT
type instance Trich D5 D5 = EQ
type instance Trich D5 D6 = LT
type instance Trich D5 D7 = LT
type instance Trich D5 D8 = LT
type instance Trich D5 D9 = LT
type instance Trich D5 (yi :* yl) = LT
type instance Trich (yi :* yl) D5 = GT
type instance Trich D6 D0 = GT
type instance Trich D6 D1 = GT
type instance Trich D6 D2 = GT
type instance Trich D6 D3 = GT
type instance Trich D6 D4 = GT
type instance Trich D6 D5 = GT
type instance Trich D6 D6 = EQ
type instance Trich D6 D7 = LT
type instance Trich D6 D8 = LT
type instance Trich D6 D9 = LT
type instance Trich D6 (yi :* yl) = LT
type instance Trich (yi :* yl) D6 = GT
type instance Trich D7 D0 = GT
type instance Trich D7 D1 = GT
type instance Trich D7 D2 = GT
type instance Trich D7 D3 = GT
type instance Trich D7 D4 = GT
type instance Trich D7 D5 = GT
type instance Trich D7 D6 = GT
type instance Trich D7 D7 = EQ
type instance Trich D7 D8 = LT
type instance Trich D7 D9 = LT
type instance Trich D7 (yi :* yl) = LT
type instance Trich (yi :* yl) D7 = GT
type instance Trich D8 D0 = GT
type instance Trich D8 D1 = GT
type instance Trich D8 D2 = GT
type instance Trich D8 D3 = GT
type instance Trich D8 D4 = GT
type instance Trich D8 D5 = GT
type instance Trich D8 D6 = GT
type instance Trich D8 D7 = GT
type instance Trich D8 D8 = EQ
type instance Trich D8 D9 = LT
type instance Trich D8 (yi :* yl) = LT
type instance Trich (yi :* yl) D8 = GT
type instance Trich D9 D0 = GT
type instance Trich D9 D1 = GT
type instance Trich D9 D2 = GT
type instance Trich D9 D3 = GT
type instance Trich D9 D4 = GT
type instance Trich D9 D5 = GT
type instance Trich D9 D6 = GT
type instance Trich D9 D7 = GT
type instance Trich D9 D8 = GT
type instance Trich D9 D9 = EQ
type instance Trich D9 (yi :* yl) = LT
type instance Trich (yi :* yl) D9 = GT
type instance Trich (xd :* xm) (yd :* ym) = CS (Trich xd yd) (Trich xm ym)
type family CS c1 c2
type instance CS EQ r = r
type instance CS GT r = GT
type instance CS LT r = LT
type family NatEq x y
type instance NatEq x y = OrderingEq (Trich x y) EQ
type family x :>: y
type instance x :>: y = OrderingEq (Trich x y) GT
(>) :: x -> y -> x :>: y
(>) = undefined
type family x :<: y
type instance x :<: y = OrderingEq (Trich x y) LT
(<) :: x -> y -> x :<: y
(<) = undefined
type family x :>=: y
type instance x :>=: y = (Succ x) :>: y
(>=) :: x -> y -> x :>=: y
(>=) = undefined
type family x :<=: y
type instance x :<=: y = x :<: (Succ y)
(<=) :: x -> y -> x :<=: y
(<=) = undefined
type family Max x y
type instance Max x y = Cond (x :>: y) x y
type family Min x y
type instance Min x y = Cond (x :<=: y) x y
max :: x -> y -> Max x y
max = undefined
min :: x -> y -> Min x y
min = undefined
type family GCD x y
type instance GCD x y = GCD' x y (IsZero y) (Trich x y)
type family GCD' x y ys cmp
type instance GCD' x D0 True cmp = D0
type instance GCD' x y False LT = GCD y x
type instance GCD' x y False EQ = x
type instance GCD' x y False GT = GCD (Sub x y) y
gcd :: x -> y -> GCD x y
gcd = undefined
type family IsZero n
type instance IsZero D0 = True
type instance IsZero D1 = False
type instance IsZero D2 = False
type instance IsZero D3 = False
type instance IsZero D4 = False
type instance IsZero D5 = False
type instance IsZero D6 = False
type instance IsZero D7 = False
type instance IsZero D8 = False
type instance IsZero D9 = False
type instance IsZero (xd:*xm) = And (IsZero xd) (IsZero xm)
type family Cond b x y
type instance Cond True x y = x
type instance Cond False x y = y