{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Type.Data.Num
    ( Negate
    , negate
    , IsPositive
    , isPositive
    , IsZero
    , isZero
    , IsNegative
    , isNegative
    , IsNatural
    , isNatural
    , One
    , one
    , Succ
    , succ
    , Pred
    , pred
    , IsEven
    , isEven
    , IsOdd
    , isOdd
    , (:+:)
    , add
    , (:-:)
    , sub
    , (:*:)
    , mul
    , Mul2
    , mul2
    , Pow2
    , pow2
    , Log2Ceil
    , log2Ceil
    , DivMod
    , divMod
    , Div
    , div
    , Mod
    , mod
    , Div2
    , div2
    , Fac
    , fac
    , Singleton(..)
    , Representation (..)
    , Integer (..)
    , Natural
    , Positive
    , Negative
    , integerFromSingleton
    , integralFromSingleton
    , singletonFromProxy
    , integralFromProxy
    , fromInteger
    , reifyPositive
    , reifyNegative
    , reifyNatural
    ) where

import Type.Data.Bool (False, True, Not)
import Type.Base.Proxy (Proxy(Proxy))
import Data.Maybe.HT (toMaybe)

import qualified Prelude as P
import Prelude (Num, Maybe, (.), (<), (>), (>=))


-- | @Negate x@ evaluates to the additive inverse of (i.e., minus) @x@.
type family Negate x
negate :: Proxy x -> Proxy (Negate x)
negate :: Proxy x -> Proxy (Negate x)
negate Proxy x
Proxy = Proxy (Negate x)
forall a. Proxy a
Proxy

type family IsPositive x
isPositive :: Proxy x -> Proxy (IsPositive x)
isPositive :: Proxy x -> Proxy (IsPositive x)
isPositive Proxy x
Proxy = Proxy (IsPositive x)
forall a. Proxy a
Proxy

type family IsZero x
isZero :: Proxy x -> Proxy (IsZero x)
isZero :: Proxy x -> Proxy (IsZero x)
isZero Proxy x
Proxy = Proxy (IsZero x)
forall a. Proxy a
Proxy

type family IsNegative x
isNegative :: Proxy x -> Proxy (IsNegative x)
isNegative :: Proxy x -> Proxy (IsNegative x)
isNegative Proxy x
Proxy = Proxy (IsNegative x)
forall a. Proxy a
Proxy

type family IsNatural x
isNatural :: Proxy x -> Proxy (IsNatural x)
isNatural :: Proxy x -> Proxy (IsNatural x)
isNatural Proxy x
Proxy = Proxy (IsNatural x)
forall a. Proxy a
Proxy

type family One repr
one :: Proxy repr -> Proxy (One repr)
one :: Proxy repr -> Proxy (One repr)
one Proxy repr
Proxy = Proxy (One repr)
forall a. Proxy a
Proxy

type family Succ x
succ :: Proxy x -> Proxy (Succ x)
succ :: Proxy x -> Proxy (Succ x)
succ Proxy x
Proxy = Proxy (Succ x)
forall a. Proxy a
Proxy

type family Pred x
pred :: Proxy x -> Proxy (Pred x)
pred :: Proxy x -> Proxy (Pred x)
pred Proxy x
Proxy = Proxy (Pred x)
forall a. Proxy a
Proxy

type family IsEven x
isEven :: Proxy x -> Proxy (IsEven x)
isEven :: Proxy x -> Proxy (IsEven x)
isEven Proxy x
Proxy = Proxy (IsEven x)
forall a. Proxy a
Proxy

type family IsOdd x
type instance IsOdd x = Not (IsEven x)
isOdd :: Proxy x -> Proxy (IsOdd x)
isOdd :: Proxy x -> Proxy (IsOdd x)
isOdd Proxy x
Proxy = Proxy (IsOdd x)
forall a. Proxy a
Proxy

type family x :+: y
add :: Proxy x -> Proxy y -> Proxy (x :+: y)
add :: Proxy x -> Proxy y -> Proxy (x :+: y)
add Proxy x
Proxy Proxy y
Proxy = Proxy (x :+: y)
forall a. Proxy a
Proxy

type family x :-: y
sub :: Proxy x -> Proxy y -> Proxy (x :-: y)
sub :: Proxy x -> Proxy y -> Proxy (x :-: y)
sub Proxy x
Proxy Proxy y
Proxy = Proxy (x :-: y)
forall a. Proxy a
Proxy

type family x :*: y
mul :: Proxy x -> Proxy y -> Proxy (x :*: y)
mul :: Proxy x -> Proxy y -> Proxy (x :*: y)
mul Proxy x
Proxy Proxy y
Proxy = Proxy (x :*: y)
forall a. Proxy a
Proxy

type family Mul2 x
mul2 :: Proxy x -> Proxy (Mul2 x)
mul2 :: Proxy x -> Proxy (Mul2 x)
mul2 Proxy x
Proxy = Proxy (Mul2 x)
forall a. Proxy a
Proxy

type family DivMod x y
divMod :: Proxy x -> Proxy y -> Proxy (DivMod x y)
divMod :: Proxy x -> Proxy y -> Proxy (DivMod x y)
divMod Proxy x
Proxy Proxy y
Proxy = Proxy (DivMod x y)
forall a. Proxy a
Proxy

type family Div x y
div :: Proxy x -> Proxy y -> Proxy (Div x y)
div :: Proxy x -> Proxy y -> Proxy (Div x y)
div Proxy x
Proxy Proxy y
Proxy = Proxy (Div x y)
forall a. Proxy a
Proxy

type family Mod x y
mod :: Proxy x -> Proxy y -> Proxy (Mod x y)
mod :: Proxy x -> Proxy y -> Proxy (Mod x y)
mod Proxy x
Proxy Proxy y
Proxy = Proxy (Mod x y)
forall a. Proxy a
Proxy

type family Div2 x
div2 :: Proxy x -> Proxy (Div2 x)
div2 :: Proxy x -> Proxy (Div2 x)
div2 Proxy x
Proxy = Proxy (Div2 x)
forall a. Proxy a
Proxy

type family Fac x
fac :: Proxy x -> Proxy (Fac x)
fac :: Proxy x -> Proxy (Fac x)
fac Proxy x
Proxy = Proxy (Fac x)
forall a. Proxy a
Proxy

type instance Fac x = FacRec x (IsZero x)
type family FacRec x is0
type instance FacRec x True = One (Repr x)
-- peasant multiplication is faster if second factor is small
type instance FacRec x False = Fac (Pred x) :*: x



type family Pow2 x
pow2 :: Proxy x -> Proxy (Pow2 x)
pow2 :: Proxy x -> Proxy (Pow2 x)
pow2 Proxy x
Proxy = Proxy (Pow2 x)
forall a. Proxy a
Proxy

type family Log2Ceil x
log2Ceil :: Proxy x -> Proxy (Log2Ceil x)
log2Ceil :: Proxy x -> Proxy (Log2Ceil x)
log2Ceil Proxy x
Proxy = Proxy (Log2Ceil x)
forall a. Proxy a
Proxy

class Integer x => Natural x
instance (Integer x, IsNatural x  ~ True) => Natural x
class Integer x => Positive x
instance (Integer x, IsPositive x ~ True) => Positive x
class Integer x => Negative x
instance (Integer x, IsNegative x ~ True) => Negative x

class (Representation (Repr x)) => Integer x where
    singleton :: Singleton x
    type Repr x

class Representation r where
    reifyIntegral ::
        Proxy r -> P.Integer ->
        (forall s. (Integer s, Repr s ~ r) => Proxy s -> a) ->
        a


newtype Singleton d = Singleton P.Integer


integerFromSingleton :: (Integer x) => Singleton x -> P.Integer
integerFromSingleton :: Singleton x -> Integer
integerFromSingleton (Singleton Integer
n) = Integer
n

integralFromSingleton :: (Integer x, Num y) => Singleton x -> y
integralFromSingleton :: Singleton x -> y
integralFromSingleton = Integer -> y
forall a. Num a => Integer -> a
P.fromInteger (Integer -> y) -> (Singleton x -> Integer) -> Singleton x -> y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Singleton x -> Integer
forall x. Integer x => Singleton x -> Integer
integerFromSingleton

singletonFromProxy :: (Integer x) => Proxy x -> Singleton x
singletonFromProxy :: Proxy x -> Singleton x
singletonFromProxy Proxy x
Proxy = Singleton x
forall x. Integer x => Singleton x
singleton

integralFromProxy :: (Integer x, Num y) => Proxy x -> y
integralFromProxy :: Proxy x -> y
integralFromProxy = Singleton x -> y
forall x y. (Integer x, Num y) => Singleton x -> y
integralFromSingleton (Singleton x -> y) -> (Proxy x -> Singleton x) -> Proxy x -> y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy x -> Singleton x
forall x. Integer x => Proxy x -> Singleton x
singletonFromProxy

-- | synonym for 'integralFromProxy', kept for backward compatibility
fromInteger :: (Integer x, Num y) => Proxy x -> y
fromInteger :: Proxy x -> y
fromInteger = Proxy x -> y
forall x y. (Integer x, Num y) => Proxy x -> y
integralFromProxy


--- positive and negative assertions: unsafe, in a trusted kernel
data AssertPos x
data AssertNeg x
data AssertNat x

assertPos :: Proxy x -> Proxy (AssertPos x)
assertPos :: Proxy x -> Proxy (AssertPos x)
assertPos Proxy x
Proxy = Proxy (AssertPos x)
forall a. Proxy a
Proxy

assertNeg :: Proxy x -> Proxy (AssertNeg x)
assertNeg :: Proxy x -> Proxy (AssertNeg x)
assertNeg Proxy x
Proxy = Proxy (AssertNeg x)
forall a. Proxy a
Proxy

assertNat :: Proxy x -> Proxy (AssertNat x)
assertNat :: Proxy x -> Proxy (AssertNat x)
assertNat Proxy x
Proxy = Proxy (AssertNat x)
forall a. Proxy a
Proxy

type instance IsPositive (AssertPos _x) = True
type instance IsPositive (AssertNeg _x) = False

type instance IsNegative (AssertPos _x) = False
type instance IsNegative (AssertNeg _x) = True
type instance IsNegative (AssertNat _x) = False

type instance IsNatural  (AssertPos _x) = True
type instance IsNatural  (AssertNeg _x) = False
type instance IsNatural  (AssertNat _x) = True

instance Integer x => Integer (AssertPos x) where 
    singleton :: Singleton (AssertPos x)
singleton = case Singleton x
forall x. Integer x => Singleton x
singleton :: Singleton x of Singleton Integer
n -> Integer -> Singleton (AssertPos x)
forall d. Integer -> Singleton d
Singleton Integer
n
    type Repr (AssertPos x) = Repr x

instance Integer x => Integer (AssertNeg x) where
    singleton :: Singleton (AssertNeg x)
singleton = case Singleton x
forall x. Integer x => Singleton x
singleton :: Singleton x of Singleton Integer
n -> Integer -> Singleton (AssertNeg x)
forall d. Integer -> Singleton d
Singleton Integer
n
    type Repr (AssertNeg x) = Repr x

instance Integer x => Integer (AssertNat x) where
    singleton :: Singleton (AssertNat x)
singleton = case Singleton x
forall x. Integer x => Singleton x
singleton :: Singleton x of Singleton Integer
n -> Integer -> Singleton (AssertNat x)
forall d. Integer -> Singleton d
Singleton Integer
n
    type Repr (AssertNat x) = Repr x

reifyPositive ::
    Representation r =>
    Proxy r -> P.Integer ->
    (forall s. (Positive s, Repr s ~ r) => Proxy s -> a) ->
    Maybe a
reifyPositive :: Proxy r
-> Integer
-> (forall s. (Positive s, Repr s ~ r) => Proxy s -> a)
-> Maybe a
reifyPositive Proxy r
r Integer
n forall s. (Positive s, Repr s ~ r) => Proxy s -> a
k =
    Bool -> a -> Maybe a
forall a. Bool -> a -> Maybe a
toMaybe (Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0) (Proxy r
-> Integer
-> (forall s. (Integer s, Repr s ~ r) => Proxy s -> a)
-> a
forall r a.
Representation r =>
Proxy r
-> Integer
-> (forall s. (Integer s, Repr s ~ r) => Proxy s -> a)
-> a
reifyIntegral Proxy r
r Integer
n (Proxy (AssertPos s) -> a
forall s. (Positive s, Repr s ~ r) => Proxy s -> a
k (Proxy (AssertPos s) -> a)
-> (Proxy s -> Proxy (AssertPos s)) -> Proxy s -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> Proxy (AssertPos s)
forall x. Proxy x -> Proxy (AssertPos x)
assertPos))

reifyNegative ::
    Representation r =>
    Proxy r -> P.Integer ->
    (forall s. (Negative s, Repr s ~ r) => Proxy s -> a) ->
    Maybe a
reifyNegative :: Proxy r
-> Integer
-> (forall s. (Negative s, Repr s ~ r) => Proxy s -> a)
-> Maybe a
reifyNegative Proxy r
r Integer
n forall s. (Negative s, Repr s ~ r) => Proxy s -> a
k =
    Bool -> a -> Maybe a
forall a. Bool -> a -> Maybe a
toMaybe (Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) (Proxy r
-> Integer
-> (forall s. (Integer s, Repr s ~ r) => Proxy s -> a)
-> a
forall r a.
Representation r =>
Proxy r
-> Integer
-> (forall s. (Integer s, Repr s ~ r) => Proxy s -> a)
-> a
reifyIntegral Proxy r
r Integer
n (Proxy (AssertNeg s) -> a
forall s. (Negative s, Repr s ~ r) => Proxy s -> a
k (Proxy (AssertNeg s) -> a)
-> (Proxy s -> Proxy (AssertNeg s)) -> Proxy s -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> Proxy (AssertNeg s)
forall x. Proxy x -> Proxy (AssertNeg x)
assertNeg))

reifyNatural ::
    Representation r =>
    Proxy r -> P.Integer ->
    (forall s. (Natural s, Repr s ~ r) => Proxy s -> a) ->
    Maybe a
reifyNatural :: Proxy r
-> Integer
-> (forall s. (Natural s, Repr s ~ r) => Proxy s -> a)
-> Maybe a
reifyNatural Proxy r
r Integer
n forall s. (Natural s, Repr s ~ r) => Proxy s -> a
k =
    Bool -> a -> Maybe a
forall a. Bool -> a -> Maybe a
toMaybe (Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0) (Proxy r
-> Integer
-> (forall s. (Integer s, Repr s ~ r) => Proxy s -> a)
-> a
forall r a.
Representation r =>
Proxy r
-> Integer
-> (forall s. (Integer s, Repr s ~ r) => Proxy s -> a)
-> a
reifyIntegral Proxy r
r Integer
n (Proxy (AssertNat s) -> a
forall s. (Natural s, Repr s ~ r) => Proxy s -> a
k (Proxy (AssertNat s) -> a)
-> (Proxy s -> Proxy (AssertNat s)) -> Proxy s -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy s -> Proxy (AssertNat s)
forall x. Proxy x -> Proxy (AssertNat x)
assertNat))